Let n be given.

Assume Hn: nat_p n.

We prove the intermediate claim Hnn: equip n n.

An exact proof term for the current goal is (equip_ref n).

An exact proof term for the current goal is (equip_finite_Power n Hn n Hnn).

∎