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: ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x5 x6 = x4 x5 x6) ⟶ x0 x1 x4 x3 = x0 x1 x2 x3.

Apply unknownprop_3bd6f6e5afa239de2bed4c5d0a7e768286a329bd2689d74ed28c7c62d231db6f with x1, x2, x3, λ x4 x5 . x0 x4 (e3162.. (f482f.. (96158.. x1 x2 x3) (4ae4a.. 4a7ef..))) (f482f.. (96158.. x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) = x0 x1 x2 x3.

Apply unknownprop_22fa583cdd675dc491864c4bc88d6afb2cb2c5c899f3088bafeb1dd37fbf3527 with x1, x2, x3, λ x4 x5 . x0 x1 (e3162.. (f482f.. (96158.. x1 x2 x3) (4ae4a.. 4a7ef..))) x4 = x0 x1 x2 x3.

Apply H0 with e3162.. (f482f.. (96158.. x1 x2 x3) (4ae4a.. 4a7ef..)).

The subproof is completed by applying unknownprop_aec86eb4da68e7f79235ce435d2568a1f89bad923e23fefb04b9885bd4542138 with x1, x2, x3.

■

Proofgold Proof