Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: nat_p x0. Let x1 of type ο be given. Assume H1: ∀ x2 . and (x2 ∈ omega) (equip x0 x2) ⟶ x1. Apply H1 with x0. Apply andI with x0 ∈ omega, equip x0 x0 leaving 2 subgoals. Apply nat_p_omega with x0. The subproof is completed by applying H0. The subproof is completed by applying equip_ref with x0. ■