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

We use 0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is nat_p_omega 0 nat_0.

Apply equip_ref to the current goal.

∎