Let x0 of type ι → ι → CT2 ι be given.

Assume H0: ∀ x1 . 80242.. x1 ⟶ ∀ x2 . 80242.. x2 ⟶ ∀ x3 x4 : ι → ι → ι . (∀ x5 . prim1 x5 (56ded.. (e4431.. x1)) ⟶ ∀ x6 . 80242.. x6 ⟶ x3 x5 x6 = x4 x5 x6) ⟶ (∀ x5 . prim1 x5 (56ded.. (e4431.. x2)) ⟶ x3 x1 x5 = x4 x1 x5) ⟶ x0 x1 x2 x3 = x0 x1 x2 x4.

Let x1 of type ι be given.

Assume H1: 80242.. x1.

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

Claim L2: ∀ x3 . 80242.. x3 ⟶ ∀ x4 x5 : ι → ι . (∀ x6 . prim1 x6 (56ded.. (e4431.. x3)) ⟶ x4 x6 = x5 x6) ⟶ (λ x6 . λ x7 : ι → ι → ι . λ x8 . λ x9 : ι → ι . x0 x6 x8 (λ x10 x11 . If_i (x10 = x6) (x9 x11) (x7 x10 x11))) x1 x2 x3 x4 = (λ x6 . λ x7 : ι → ι → ι . λ x8 . λ x9 : ι → ι . x0 x6 x8 (λ x10 x11 . If_i (x10 = x6) (x9 x11) (x7 x10 x11))) x1 x2 x3 x5

Let x3 of type ι be given.

Assume H2: 80242.. x3.

Let x4 of type ι → ι be given.

Let x5 of type ι → ι be given.

Assume H3: ∀ x6 . prim1 x6 (56ded.. (e4431.. x3)) ⟶ x4 x6 = x5 x6.

Claim L4: ∀ x6 . prim1 x6 (56ded.. (e4431.. x1)) ⟶ x2 x6 = x2 x6

Let x6 of type ι be given.

Assume H4: prim1 x6 (56ded.. (e4431.. x1)).

Let x7 of type (ι → ι) → (ι → ι) → ο be given.

Assume H5: x7 (x2 x6) (x2 x6).

The subproof is completed by applying H5.

Apply unknownprop_e0c85cee9ac65183fa23d59dc9bf803545072536a7d1ab844f5f6ba67d85070e with x0, x1, x2, x2, x3, x4, x5 leaving 5 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying L4.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

Apply unknownprop_db769b563873789c738c81339939934774194105a1bb9dc7e2f35973f52f11f3 with (λ x3 . λ x4 : ι → ι → ι . λ x5 . λ x6 : ι → ι . x0 x3 x5 (λ x7 x8 . If_i (x7 = x3) (x6 x8) (x4 x7 x8))) x1 x2.

The subproof is completed by applying L2.

■

Proofgold Proof