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) ⟶ ∀ x9 : ι → ι . (∀ x10 . prim1 x10 x1 ⟶ x5 x10 = x9 x10) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_082939bedfe14cadfd82477d99c5c424f448e3091a657bed109ed74edc778e6f with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (e3162.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x0 x1 x2 x3 x4 x5.
Apply H0 with
e3162.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
e3162.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
e3162.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
f482f.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_93ad6d9e989b43148688f9a96022108d8fdf2fbb96408fca4e828dbfbae29330 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_6dd8f55228cd05752343b8ca499fb011022efaaaa36500a4a4d7ce24e9f31c71 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_4af70ca0b99321d573ec535c595ae3567a5a5d4e2f63e06366bc0778b1598496 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_cc6313a53ab35f7dac5cbbd7a5c325ad7f853ba4d0f96a1e99248aff054ca448 with x1, x2, x3, x4, x5.