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 ⟶ ∀ x10 . prim1 x10 x1 ⟶ x4 x9 x10 = x8 x9 x10) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_74aeb2b31565ab559dd862503d77281dfaa45772666c82759a1164825097bf34 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (e3162.. (f482f.. (71338.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (71338.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. (71338.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (71338.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_7fa7a5a74cf161314fac31f56afe4de41cd061d38975b981f056e284178787d5 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (e3162.. (f482f.. (71338.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (71338.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. (71338.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
e3162.. (f482f.. (71338.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (71338.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
e3162.. (f482f.. (71338.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_9b454a2a80798cd0556f866bae028da0e2e318c1ba057a70c632226789ea8a84 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_f31aaef5c858e3702eb2359462a8937983338781aa537e061f9d5fdc0f57e20d with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_e54ba49d9a3e3d8a71364e79ce9fdb2e0cc0dda16726fbe8dee22a1930324832 with x1, x2, x3, x4, x5.