Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: nat_p x1.

Assume H1: atleastp x0 x1.

Apply unknownprop_4bfbb4dec5e67ad21ca2193ea2b4908e823372bc7bdc402dd93e056c69cdf1ed with x0, x1, ∃ x2 . and (In x2 (ordsucc x1)) (equip x0 x2) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H2: (λ x3 . and (Subq x3 x1) (equip x0 x3)) x2.

Apply andE with Subq x2 x1, equip x0 x2, ∃ x3 . and (In x3 (ordsucc x1)) (equip x0 x3) leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H3: Subq x2 x1.

Assume H4: equip x0 x2.

Apply unknownprop_fcf2ff654d67a068f6413fb39e7210317502e60a1c216efa9e014e79c6c67d1f with x1, x2, ∃ x3 . and (In x3 (ordsucc x1)) (equip x0 x3) leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

Let x3 of type ι be given.

Assume H5: (λ x4 . and (In x4 (ordsucc x1)) (equip x2 x4)) x3.

Apply andE with In x3 (ordsucc x1), equip x2 x3, ∃ x4 . and (In x4 (ordsucc x1)) (equip x0 x4) leaving 2 subgoals.

The subproof is completed by applying H5.

Assume H6: In x3 (ordsucc x1).

Assume H7: equip x2 x3.

Let x4 of type ο be given.

Assume H8: ∀ x5 . and (In x5 (ordsucc x1)) (equip x0 x5) ⟶ x4.

Apply H8 with x3.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In x3 (ordsucc x1), equip x0 x3 leaving 2 subgoals.

The subproof is completed by applying H6.

Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with x0, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H7.

■

Proofgold Proof