Let x0 of type ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → ο be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι be given.
Let x4 of type ι → ι be given.
Assume H0:
∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x4 x8 = x7 x8) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4.
Apply unknownprop_d3b5acfee106d0e14fe58094c8e3c6f75e54c07e6481b9e36207e34ac8236fe5 with
x1,
x2,
x3,
x4,
λ x5 x6 . x0 x5 (e3162.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4.
Apply H0 with
e3162.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
f482f.. (f482f.. (a255b.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_8158cb53a6ed2c6ca20129fda5153cb308dc2ca6e90a584aa8a3f15eb6f871ea with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_6240d82b92741e6cbf5c66460b7082bc5753da2dd534074b46e0f43ee9335cf6 with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_ea68f7a822834285aec4e0837699a1b95f35c6b4c76e31caccc8a9483647132a with x1, x2, x3, x4.