Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: 69b7e.. x0 x1.

Let x2 of type ι → ι → ο be given.

Assume H1: ∀ x3 x4 . ∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x4 ⟶ ∀ x7 . prim1 x7 x4 ⟶ prim1 (x5 x6 x7) x4) ⟶ 4f2b4.. (987b2.. x3 x5) ⟶ Subq x3 x4 ⟶ x2 (987b2.. x3 x5) (987b2.. x4 x5).

Apply H0 with x2 x0 x1.

Assume H2: and (30750.. x1) (30750.. x0).

Assume H3: 93c99.. x1 (λ x3 . λ x4 : ι → ι → ι . 93c99.. x0 (λ x5 . λ x6 : ι → ι → ι . and (and (x0 = 987b2.. x5 x4) (4f2b4.. (987b2.. x5 x4))) (Subq x5 x3))).

Apply H2 with x2 x0 x1.

Assume H4: 30750.. x1.

Assume H5: 30750.. x0.

Claim L6: 69b7e.. x0 x1 ⟶ x2 x0 x1

Apply H4 with λ x3 . 69b7e.. x0 x3 ⟶ x2 x0 x3.

Let x3 of type ι be given.

Let x4 of type ι → ι → ι be given.

Assume H6: ∀ x5 . prim1 x5 x3 ⟶ ∀ x6 . prim1 x6 x3 ⟶ prim1 (x4 x5 x6) x3.

Apply H5 with λ x5 . 69b7e.. x5 (987b2.. x3 x4) ⟶ x2 x5 (987b2.. x3 x4).

Let x5 of type ι be given.

Let x6 of type ι → ι → ι be given.

Assume H7: ∀ x7 . prim1 x7 x5 ⟶ ∀ x8 . prim1 x8 x5 ⟶ prim1 (x6 x7 x8) x5.

Assume H8: 69b7e.. (987b2.. x5 x6) (987b2.. x3 x4).

Apply unknownprop_8a8b3072385f65c851385b35246a4b711e6bd63000d15cc8311a66f73fe8acbb with x5, x3, x6, x4, x2 (987b2.. x5 x6) (987b2.. x3 x4) leaving 2 subgoals.

The subproof is completed by applying H8.

Assume H9: 987b2.. x5 x6 = 987b2.. x5 x4.

Assume H10: 7fe8f.. x3 x4 x5.

Apply H10 with x2 (987b2.. x5 x6) (987b2.. x3 x4).

Assume H11: 4f2b4.. (987b2.. x5 x4).

Assume H12: Subq x5 x3.

Apply H9 with λ x7 x8 . x2 x8 (987b2.. x3 x4).

Apply H1 with x5, x3, x4 leaving 3 subgoals.

The subproof is completed by applying H6.

The subproof is completed by applying H11.

The subproof is completed by applying H12.

Apply L6.

The subproof is completed by applying H0.

■

Proofgold Proof