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.
Let x5 of type ι → ι be given.
Assume H0:
∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι . (∀ x9 . prim1 x9 x1 ⟶ x4 x9 = x8 x9) ⟶ ∀ x9 : ι → ι . (∀ x10 . prim1 x10 x1 ⟶ x5 x10 = x9 x10) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_3a664dd9c5a855abda39bdd71b735612c33924fca66e1d86341cec92d11c1905 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (e3162.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x0 x1 x2 x3 x4 x5.
Apply H0 with
e3162.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
f482f.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
f482f.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_9be526f58304e3f48c68552cb7dab77faeadeafbfe6f61016e30a5f7e836121a with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_b1594d2d06a5df0c18732ad3e5e183932a298887b056759ac66539b732277e19 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_f5d91be8be621c43c23c5c2fda28f2cb6c5898bbe5f2d6b1bb2e76a774efe261 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_538cbd722c7faac916933f735806a209a15d840ed1e26c5746cb263bfec2ab2e with x1, x2, x3, x4, x5.