Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: 02b90.. x0 x1.

Apply H0 with 02b90.. (94f9e.. x1 (λ x2 . f4dc0.. x2)) (94f9e.. x0 (λ x2 . f4dc0.. x2)).

Assume H1: and (∀ x2 . prim1 x2 x0 ⟶ 80242.. x2) (∀ x2 . prim1 x2 x1 ⟶ 80242.. x2).

Apply H1 with (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3) ⟶ 02b90.. (94f9e.. x1 (λ x2 . f4dc0.. x2)) (94f9e.. x0 (λ x2 . f4dc0.. x2)).

Assume H2: ∀ x2 . prim1 x2 x0 ⟶ 80242.. x2.

Assume H3: ∀ x2 . prim1 x2 x1 ⟶ 80242.. x2.

Assume H4: ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3.

Apply and3I with ∀ x2 . prim1 x2 (94f9e.. x1 (λ x3 . f4dc0.. x3)) ⟶ 80242.. x2, ∀ x2 . prim1 x2 (94f9e.. x0 (λ x3 . f4dc0.. x3)) ⟶ 80242.. x2, ∀ x2 . prim1 x2 (94f9e.. x1 (λ x3 . f4dc0.. x3)) ⟶ ∀ x3 . prim1 x3 (94f9e.. x0 (λ x4 . f4dc0.. x4)) ⟶ 099f3.. x2 x3 leaving 3 subgoals.

Let x2 of type ι be given.

Assume H5: prim1 x2 (94f9e.. x1 (λ x3 . f4dc0.. x3)).

Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with x1, λ x3 . f4dc0.. x3, x2, 80242.. x2 leaving 2 subgoals.

The subproof is completed by applying H5.

Let x3 of type ι be given.

Assume H6: prim1 x3 x1.

Assume H7: x2 = f4dc0.. x3.

Apply H7 with λ x4 x5 . 80242.. x5.

Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with x3.

Apply H3 with x3.

The subproof is completed by applying H6.

Let x2 of type ι be given.

Assume H5: prim1 x2 (94f9e.. x0 (λ x3 . f4dc0.. x3)).

Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with x0, λ x3 . f4dc0.. x3, x2, 80242.. x2 leaving 2 subgoals.

The subproof is completed by applying H5.

Let x3 of type ι be given.

Assume H6: prim1 x3 x0.

Assume H7: x2 = f4dc0.. x3.

Apply H7 with λ x4 x5 . 80242.. x5.

Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with x3.

Apply H2 with x3.

The subproof is completed by applying H6.

Let x2 of type ι be given.

Assume H5: prim1 x2 (94f9e.. x1 (λ x3 . f4dc0.. x3)).

Let x3 of type ι be given.

Assume H6: prim1 x3 (94f9e.. x0 (λ x4 . f4dc0.. x4)).

Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with x1, λ x4 . f4dc0.. x4, x2, 099f3.. x2 x3 leaving 2 subgoals.

The subproof is completed by applying H5.

Let x4 of type ι be given.

Assume H7: prim1 x4 x1.

Assume H8: x2 = f4dc0.. x4.

Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with x0, λ x5 . f4dc0.. x5, x3, 099f3.. x2 x3 leaving 2 subgoals.

The subproof is completed by applying H6.

Let x5 of type ι be given.

Assume H9: prim1 x5 x0.

Assume H10: x3 = f4dc0.. x5.

Apply H8 with λ x6 x7 . 099f3.. x7 x3.

Apply H10 with λ x6 x7 . 099f3.. (f4dc0.. x4) x7.

Apply unknownprop_3cc82c9758d3882690e6647e4154486613d1a5c615c0651627364410273ab026 with x5, x4 leaving 3 subgoals.

Apply H2 with x5.

The subproof is completed by applying H9.

Apply H3 with x4.

The subproof is completed by applying H7.

Apply H4 with x5, x4 leaving 2 subgoals.

The subproof is completed by applying H9.

The subproof is completed by applying H7.

■

Proofgold Proof