Let n be given.

Assume Hn: nat_p n.

We will prove ∃n' ∈ ω, equip n n'.

We use n to witness the existential quantifier.

Apply andI to the current goal.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is Hn.

We will prove equip n n.

Apply equip_ref to the current goal.

∎