Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Let x1 of type (ι → ι → ι → ι → ι → ι → ι) → ο be given.
Apply H0 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . (Church6_lt4p x2 ⟶ x1 x2) ⟶ x1 (λ x3 x4 x5 x6 x7 x8 . x7) ⟶ x1 (λ x3 x4 x5 x6 x7 x8 . x8) ⟶ x1 x2 leaving 6 subgoals.
Assume H1:
Church6_lt4p (λ x2 x3 x4 x5 x6 x7 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x2).
Assume H2: x1 (λ x2 x3 x4 x5 x6 x7 . x6).
Assume H3: x1 (λ x2 x3 x4 x5 x6 x7 . x7).
Apply H1.
The subproof is completed by applying unknownprop_56ce56513a8af1327555b873c1c6ce07e295bb2d93a34f831bbfdb3328f2809b.
Assume H1:
Church6_lt4p (λ x2 x3 x4 x5 x6 x7 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x3).
Assume H2: x1 (λ x2 x3 x4 x5 x6 x7 . x6).
Assume H3: x1 (λ x2 x3 x4 x5 x6 x7 . x7).
Apply H1.
The subproof is completed by applying unknownprop_995579645b8886904e46af0dc0ac8e19ee3cd4af7d78809ff698344ead396f5a.
Assume H1:
Church6_lt4p (λ x2 x3 x4 x5 x6 x7 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x4).
Assume H2: x1 (λ x2 x3 x4 x5 x6 x7 . x6).
Assume H3: x1 (λ x2 x3 x4 x5 x6 x7 . x7).
Apply H1.
The subproof is completed by applying unknownprop_bd8f81a1227d0cc25cea7c364f7541293f70705efd4999ad0dba8cf8857226a9.
Assume H1:
Church6_lt4p (λ x2 x3 x4 x5 x6 x7 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x5).
Assume H2: x1 (λ x2 x3 x4 x5 x6 x7 . x6).
Assume H3: x1 (λ x2 x3 x4 x5 x6 x7 . x7).
Apply H1.
The subproof is completed by applying unknownprop_9ab406e767d5138f84eceb89ae815ef2f93656cc034576ca18ab84af7a608607.
Assume H1:
Church6_lt4p (λ x2 x3 x4 x5 x6 x7 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x6).
Assume H2: x1 (λ x2 x3 x4 x5 x6 x7 . x6).
Assume H3: x1 (λ x2 x3 x4 x5 x6 x7 . x7).
The subproof is completed by applying H2.
Assume H1:
Church6_lt4p (λ x2 x3 x4 x5 x6 x7 . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x7).
Assume H2: x1 (λ x2 x3 x4 x5 x6 x7 . x6).
Assume H3: x1 (λ x2 x3 x4 x5 x6 x7 . x7).
The subproof is completed by applying H3.