Let x0 of type ι → ο be given.
Let x1 of type ι → ι → ι → ο be given.
Let x2 of type ι → ι be given.
Let x3 of type ι → ι → ι → ι → ι → ι be given.
Apply unknownprop_795e291855a044d4d636c961caa1600704603cc02e33a7b37aa66e8d7f6512db with
x0,
x1,
x2,
x3,
x0,
x1,
x2,
x3,
λ x4 . x4,
λ x4 x5 x6 . x6 leaving 4 subgoals.
Let x4 of type ι be given.
Assume H0: x0 x4.
The subproof is completed by applying H0.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H0: x0 x4.
Assume H1: x0 x5.
Assume H2: x1 x4 x5 x6.
The subproof is completed by applying H2.
Let x4 of type ι be given.
Assume H0: x0 x4.
Let x5 of type ι → ι → ο be given.
Assume H1: x5 ((λ x6 x7 x8 . x8) x4 x4 (x2 x4)) (x2 ((λ x6 . x6) x4)).
The subproof is completed by applying H1.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H0: x0 x4.
Assume H1: x0 x5.
Assume H2: x0 x6.
Assume H3: x1 x4 x5 x7.
Assume H4: x1 x5 x6 x8.
Let x9 of type ι → ι → ο be given.
Assume H5: x9 ((λ x10 x11 x12 . x12) x4 x6 (x3 x4 x5 x6 x8 x7)) (x3 ((λ x10 . x10) x4) ((λ x10 . x10) x5) ((λ x10 . x10) x6) ((λ x10 x11 x12 . x12) x5 x6 x8) ((λ x10 x11 x12 . x12) x4 x5 x7)).
The subproof is completed by applying H5.