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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x4 x8 x9 = x7 x8 x9) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4.
Apply unknownprop_8f65da788a93ff89d95bcf516abc29daa711f2c16faefefcaad5ba81f2e71786 with
x1,
x2,
x3,
x4,
λ x5 x6 . x0 x5 (e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4.
Apply H0 with
e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))),
e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_ff4535e6de7d81b5e64319b54276975d755c6038dfc6568b8eaad6de9e67f064 with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_d91c9a6f9c15a2c6b9d2b80e56f063e4e1af105da6d9f1d5f7ab2c269bb9687a with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_d90cbda69461be2219583389e1055578190fbc4e0c943c03394d871429ab3a0a with x1, x2, x3, x4.