Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: 02b90.. x0 x1.

Assume H1: 02b90.. x2 x3.

Assume H2: ∀ x4 . prim1 x4 x0 ⟶ 099f3.. x4 (02a50.. x2 x3).

Assume H3: ∀ x4 . prim1 x4 x3 ⟶ 099f3.. (02a50.. x0 x1) x4.

Apply H0 with fe4bb.. (02a50.. x0 x1) (02a50.. x2 x3).

Assume H4: and (∀ x4 . prim1 x4 x0 ⟶ 80242.. x4) (∀ x4 . prim1 x4 x1 ⟶ 80242.. x4).

Apply H4 with (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x1 ⟶ 099f3.. x4 x5) ⟶ fe4bb.. (02a50.. x0 x1) (02a50.. x2 x3).

Assume H5: ∀ x4 . prim1 x4 x0 ⟶ 80242.. x4.

Assume H6: ∀ x4 . prim1 x4 x1 ⟶ 80242.. x4.

Assume H7: ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x1 ⟶ 099f3.. x4 x5.

Apply H1 with fe4bb.. (02a50.. x0 x1) (02a50.. x2 x3).

Assume H8: and (∀ x4 . prim1 x4 x2 ⟶ 80242.. x4) (∀ x4 . prim1 x4 x3 ⟶ 80242.. x4).

Apply H8 with (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x3 ⟶ 099f3.. x4 x5) ⟶ fe4bb.. (02a50.. x0 x1) (02a50.. x2 x3).

Assume H9: ∀ x4 . prim1 x4 x2 ⟶ 80242.. x4.

Assume H10: ∀ x4 . prim1 x4 x3 ⟶ 80242.. x4.

Assume H11: ∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x3 ⟶ 099f3.. x4 x5.

Apply unknownprop_e277188ae242e07bd6727f267e38747aecd739d129890076e65b92339f7beb98 with x0, x1, fe4bb.. (02a50.. x0 x1) (02a50.. x2 x3) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H12: and (and (and (80242.. (02a50.. x0 x1)) (prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x4 . 4ae4a.. (e4431.. x4))) (a842e.. x1 (λ x4 . 4ae4a.. (e4431.. x4))))))) (∀ x4 . prim1 x4 x0 ⟶ 099f3.. x4 (02a50.. x0 x1))) (∀ x4 . prim1 x4 x1 ⟶ 099f3.. (02a50.. x0 x1) x4).

Apply H12 with (∀ x4 . 80242.. x4 ⟶ (∀ x5 . prim1 x5 x0 ⟶ 099f3.. x5 x4) ⟶ (∀ x5 . prim1 x5 x1 ⟶ 099f3.. x4 x5) ⟶ and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x4)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x4)) ⟶ fe4bb.. (02a50.. x0 x1) (02a50.. x2 x3).

Assume H13: and (and ... ...) ....

...

■

Proofgold Proof