Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: 69b7e.. x0 x1.

Apply unknownprop_09de1147759e25fadb4f5ddd0bff1cf184e6305d39ef0b039b6fe06bc3ba5cbd with x0, x1, λ x3 x4 . 69b7e.. x4 x2 ⟶ 69b7e.. x3 x2 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x3 of type ι be given.

Let x4 of type ι be given.

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

Assume H1: ∀ x6 . prim1 x6 x4 ⟶ ∀ x7 . prim1 x7 x4 ⟶ prim1 (x5 x6 x7) x4.

Assume H2: 4f2b4.. (987b2.. x3 x5).

Assume H3: Subq x3 x4.

Assume H4: 69b7e.. (987b2.. x4 x5) x2.

Claim L5: 987b2.. x4 x5 = 987b2.. x4 x5 ⟶ 69b7e.. (987b2.. x3 x5) x2

Apply unknownprop_09de1147759e25fadb4f5ddd0bff1cf184e6305d39ef0b039b6fe06bc3ba5cbd with 987b2.. x4 x5, x2, λ x6 x7 . 987b2.. x4 x5 = x6 ⟶ 69b7e.. (987b2.. x3 x5) x7 leaving 2 subgoals.

The subproof is completed by applying H4.

Let x6 of type ι be given.

Let x7 of type ι be given.

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

Assume H5: ∀ x9 . prim1 x9 x7 ⟶ ∀ x10 . prim1 x10 x7 ⟶ prim1 (x8 x9 x10) x7.

Assume H6: 4f2b4.. (987b2.. x6 x8).

Assume H7: Subq x6 x7.

Assume H8: 987b2.. x4 x5 = 987b2.. x6 x8.

Apply unknownprop_5cd05a110f3bf2a31b9390cadb44d05e7c4e54bd01cb3a1cbe102c4d216d9b84 with x4, x6, x5, x8, 69b7e.. (987b2.. x3 x5) (987b2.. x7 x8) leaving 2 subgoals.

The subproof is completed by applying H8.

Assume H9: x4 = x6.

Assume H10: ∀ x9 . prim1 x9 x4 ⟶ ∀ x10 . prim1 x10 x4 ⟶ x5 x9 x10 = x8 x9 x10.

Claim L11: ∀ x9 . prim1 x9 x3 ⟶ ∀ x10 . prim1 x10 x3 ⟶ prim1 (x5 x9 x10) x3

Apply unknownprop_92c6fa644c6dced27956132c489750908a0c8c60a2c0fd4eb67751c9bc54bfc0 with x3, x5, ∀ x9 . ... ⟶ ∀ x10 . ... ⟶ prim1 (x5 x9 x10) ... leaving 2 subgoals.

...

Claim L12: 987b2.. x3 x5 = 987b2.. x3 x8

Apply unknownprop_d45876018bd1c8a04fed4c22e23277ef3c518489a1fd1bb4edfb07f8fb3466d0 with x3, x5, x8.

Let x9 of type ι be given.

Assume H12: prim1 x9 x3.

Let x10 of type ι be given.

Assume H13: prim1 x10 x3.

Apply H10 with x9, x10 leaving 2 subgoals.

Apply H3 with x9.

The subproof is completed by applying H12.

Apply H3 with x10.

The subproof is completed by applying H13.

Apply and3I with 30750.. (987b2.. x7 x8), 30750.. (987b2.. x3 x5), 93c99.. (987b2.. x7 x8) (λ x9 . λ x10 : ι → ι → ι . 93c99.. (987b2.. x3 x5) (λ x11 . λ x12 : ι → ι → ι . and (and (987b2.. x3 x5 = 987b2.. x11 x10) (4f2b4.. (987b2.. x11 x10))) (Subq x11 x9))) leaving 3 subgoals.

Apply unknownprop_10272f9d8a272cf914054010d8c3a4593cfbbcb7954b0a903e2d867e85e26e68 with x7, x8.

The subproof is completed by applying H5.

Apply unknownprop_10272f9d8a272cf914054010d8c3a4593cfbbcb7954b0a903e2d867e85e26e68 with x3, x5.

The subproof is completed by applying L11.

Apply unknownprop_cd20f7dbc591f4f87c87c35509dc2db382cd96f4518c628ca9882a10b2d1671d with x3, x7, x5, x8, λ x9 x10 : ο . x10.

Apply and3I with 987b2.. x3 x5 = 987b2.. x3 x8, 4f2b4.. (987b2.. x3 x8), Subq x3 x7 leaving 3 subgoals.

The subproof is completed by applying L12.

Apply L12 with λ x9 x10 . 4f2b4.. x9.

The subproof is completed by applying H2.

Let x9 of type ι be given.

Assume H13: prim1 x9 x3.

Apply H7 with x9.

Apply H9 with λ x10 x11 . prim1 x9 x10.

Apply H3 with x9.

The subproof is completed by applying H13.

Apply L5.

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

Assume H6: x6 (987b2.. x4 x5) (987b2.. x4 x5).

The subproof is completed by applying H6.

■

Proofgold Proof