Apply unknownprop_f23dde3020cfe827bdc4db0338b279dd2c0f6c90742a195a1a7a614475669076 with λ x0 . ∀ x1 : ι → ι . (∀ x2 . In x2 (ordsucc x0) ⟶ In (x1 x2) x0) ⟶ not (∀ x2 . In x2 (ordsucc x0) ⟶ ∀ x3 . In x3 (ordsucc x0) ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) leaving 2 subgoals.

Let x0 of type ι → ι be given.

Assume H0: ∀ x1 . In x1 1 ⟶ In (x0 x1) 0.

Apply FalseE with not (∀ x1 . In x1 1 ⟶ ∀ x2 . In x2 1 ⟶ x0 x1 = x0 x2 ⟶ x1 = x2).

Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with x0 0.

Apply H0 with 0.

The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 : ι → ι . (∀ x2 . In x2 (ordsucc x0) ⟶ In (x1 x2) x0) ⟶ not (∀ x2 . In x2 (ordsucc x0) ⟶ ∀ x3 . In x3 (ordsucc x0) ⟶ x1 x2 = x1 x3 ⟶ x2 = x3).

Let x1 of type ι → ι be given.

Assume H2: ∀ x2 . In x2 (ordsucc (ordsucc x0)) ⟶ In (x1 x2) (ordsucc x0).

Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with ∀ x2 . In x2 (ordsucc (ordsucc x0)) ⟶ ∀ x3 . In x3 (ordsucc (ordsucc x0)) ⟶ x1 x2 = x1 x3 ⟶ x2 = x3.

Assume H3: ∀ x2 . In x2 (ordsucc (ordsucc x0)) ⟶ ∀ x3 . In x3 (ordsucc (ordsucc x0)) ⟶ x1 x2 = x1 x3 ⟶ x2 = x3.

Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with ∃ x2 . and (In x2 (ordsucc (ordsucc x0))) (x1 x2 = x0), False leaving 2 subgoals.

Assume H4: ∃ x2 . and (In x2 (ordsucc (ordsucc x0))) (x1 x2 = x0).

Apply H4 with False.

Let x2 of type ι be given.

Assume H5: (λ x3 . and (In x3 (ordsucc (ordsucc x0))) (x1 x3 = x0)) x2.

Apply andE with In x2 (ordsucc (ordsucc x0)), x1 x2 = x0, False leaving 2 subgoals.

The subproof is completed by applying H5.

Assume H6: In x2 (ordsucc (ordsucc x0)).

Assume H7: x1 x2 = x0.

Claim L8: ...

...

Apply notE with ∀ x3 . In x3 (ordsucc x0) ⟶ ∀ x4 . In x4 (ordsucc x0) ⟶ (λ x5 . If_i (Subq x2 x5) (x1 (ordsucc x5)) (x1 x5)) x3 = (λ x5 . If_i (Subq x2 x5) (x1 (ordsucc x5)) (x1 x5)) x4 ⟶ x3 = x4 leaving 2 subgoals.

The subproof is completed by applying L8.

Let x3 of type ι be given.

Assume H9: In x3 (ordsucc x0).

Let x4 of type ι be given.

Assume H10: In x4 (ordsucc x0).

Claim L11: ...

...

Claim L12: ...

...

Claim L13: ...

...

Claim L14: ...

...

Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with Subq x2 x3, If_i (Subq x2 x3) ... ... = ... ⟶ x3 = x4 leaving 2 subgoals.

...

■

Proofgold Proof