Apply unknownprop_98dce570015dab8b9107dc33a5e2e4ea0417c490e1cfe00b91b6267d26e82089 with λ x0 x1 . e6316.. x0 x1 = e6316.. x1 x0.

Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: 80242.. x0.

Assume H1: 80242.. x1.

Assume H2: ∀ x2 . prim1 x2 (56ded.. (e4431.. x0)) ⟶ e6316.. x2 x1 = e6316.. x1 x2.

Assume H3: ∀ x2 . prim1 x2 (56ded.. (e4431.. x1)) ⟶ e6316.. x0 x2 = e6316.. x2 x0.

Assume H4: ∀ x2 . prim1 x2 (56ded.. (e4431.. x0)) ⟶ ∀ x3 . prim1 x3 (56ded.. (e4431.. x1)) ⟶ e6316.. x2 x3 = e6316.. x3 x2.

Apply unknownprop_0bba6b6e1ff88cb6fe93e4b3f72d170fee2180507070ff2fab0f5b4dc92e6b37 with x0, x1, e6316.. x0 x1 = e6316.. x1 x0 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H5: 02b90.. x2 x3.

Assume H6: ∀ x4 . prim1 x4 x2 ⟶ ∀ x5 : ο . (∀ x6 . prim1 x6 (23e07.. x0) ⟶ ∀ x7 . prim1 x7 (23e07.. x1) ⟶ x4 = bc82c.. (e6316.. x6 x1) (bc82c.. (e6316.. x0 x7) (f4dc0.. (e6316.. x6 x7))) ⟶ x5) ⟶ (∀ x6 . prim1 x6 (5246e.. x0) ⟶ ∀ x7 . prim1 x7 (5246e.. x1) ⟶ x4 = bc82c.. (e6316.. x6 x1) (bc82c.. (e6316.. x0 x7) (f4dc0.. (e6316.. x6 x7))) ⟶ x5) ⟶ x5.

Assume H7: ∀ x4 . prim1 x4 (23e07.. x0) ⟶ ∀ x5 . prim1 x5 (23e07.. x1) ⟶ prim1 (bc82c.. (e6316.. x4 x1) (bc82c.. (e6316.. x0 x5) (f4dc0.. (e6316.. x4 x5)))) x2.

Assume H8: ∀ x4 . prim1 x4 (5246e.. x0) ⟶ ∀ x5 . prim1 x5 (5246e.. x1) ⟶ prim1 (bc82c.. (e6316.. x4 x1) (bc82c.. (e6316.. x0 x5) (f4dc0.. (e6316.. x4 x5)))) x2.

Assume H9: ∀ x4 . prim1 x4 x3 ⟶ ∀ x5 : ο . (∀ x6 . prim1 x6 (23e07.. x0) ⟶ ∀ x7 . prim1 x7 (5246e.. x1) ⟶ x4 = bc82c.. (e6316.. x6 x1) (bc82c.. (e6316.. x0 x7) (f4dc0.. (e6316.. x6 x7))) ⟶ x5) ⟶ (∀ x6 . prim1 x6 (5246e.. x0) ⟶ ∀ x7 . prim1 x7 (23e07.. x1) ⟶ x4 = bc82c.. (e6316.. x6 x1) (bc82c.. (e6316.. x0 x7) (f4dc0.. (e6316.. x6 x7))) ⟶ x5) ⟶ x5.

Assume H10: ∀ x4 . ... ⟶ ∀ x5 . prim1 x5 (5246e.. ...) ⟶ prim1 (bc82c.. (e6316.. x4 x1) (bc82c.. (e6316.. x0 x5) (f4dc0.. (e6316.. x4 x5)))) x3.

...

■

Proofgold Proof