Claim L0: ∀ x0 . 80242.. x0 ⟶ ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 (56ded.. (e4431.. x0)) ⟶ x1 x3 = x2 x3) ⟶ 02a50.. (94f9e.. (5246e.. x0) (λ x3 . x1 x3)) (94f9e.. (23e07.. x0) (λ x3 . x1 x3)) = 02a50.. (94f9e.. (5246e.. x0) (λ x3 . x2 x3)) (94f9e.. (23e07.. x0) (λ x3 . x2 x3))

Let x0 of type ι be given.

Assume H0: 80242.. x0.

Let x1 of type ι → ι be given.

Let x2 of type ι → ι be given.

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

Claim L2: 94f9e.. (5246e.. x0) (λ x3 . x1 x3) = 94f9e.. (5246e.. x0) (λ x3 . x2 x3)

Apply unknownprop_59be5eee144fb0f12156456c7f9888c3f0525fea126d0d8cdf71e5c53005d86a with 5246e.. x0, λ x3 . x1 x3, λ x3 . x2 x3.

Let x3 of type ι be given.

Assume H2: prim1 x3 (5246e.. x0).

Apply H1 with x3.

Apply unknownprop_ec2b379cf3a021562909cab961365363fff9933ed29077a9b31486713164faf0 with x0, x3 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H2.

Claim L3: 94f9e.. (23e07.. x0) (λ x3 . x1 x3) = 94f9e.. (23e07.. x0) (λ x3 . x2 x3)

Apply unknownprop_59be5eee144fb0f12156456c7f9888c3f0525fea126d0d8cdf71e5c53005d86a with 23e07.. x0, λ x3 . x1 x3, λ x3 . x2 x3.

Let x3 of type ι be given.

Assume H3: prim1 x3 (23e07.. x0).

Apply H1 with x3.

Apply unknownprop_9e58dc0198eb641c42661f199c5d81a40de7e1e482f6bf245a8d8ff3d00bed34 with x0, x3 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

Apply L2 with λ x3 x4 . 02a50.. x4 (94f9e.. (23e07.. x0) (λ x5 . x1 x5)) = 02a50.. (94f9e.. (5246e.. x0) (λ x5 . x2 x5)) (94f9e.. (23e07.. x0) (λ x5 . x2 x5)).

Apply L3 with λ x3 x4 . 02a50.. (94f9e.. (5246e.. x0) (λ x5 . x2 x5)) x4 = 02a50.. (94f9e.. (5246e.. x0) (λ x5 . x2 x5)) (94f9e.. (23e07.. x0) (λ x5 . x2 x5)).

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

Assume H4: x3 (02a50.. (94f9e.. (5246e.. x0) (λ x4 . x2 x4)) (94f9e.. (23e07.. x0) (λ x4 . x2 x4))) (02a50.. (94f9e.. (5246e.. x0) (λ x4 . x2 x4)) (94f9e.. (23e07.. x0) (λ x4 . x2 x4))).

The subproof is completed by applying H4.

Apply unknownprop_db769b563873789c738c81339939934774194105a1bb9dc7e2f35973f52f11f3 with λ x0 . λ x1 : ι → ι . 02a50.. (94f9e.. (5246e.. x0) (λ x2 . x1 x2)) (94f9e.. (23e07.. x0) (λ x2 . x1 x2)).

The subproof is completed by applying L0.

■

Proofgold Proof