Let x be given.

We will prove ∃n ∈ ω, equip {x} n.

We use 1 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is nat_p_omega 1 nat_1.

An exact proof term for the current goal is equip_Sing_1 x.

∎