Let x0 of type ι → ο be given.
Let x1 of type ι → ι → ι be given.
Assume H0: ∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3).
Assume H1: ∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x1 (x1 x2 x3) x4 = x1 x2 (x1 x3 x4).
Let x2 of type ι be given.
Let x3 of type ι be given.
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.
Let x9 of type ι be given.
Let x10 of type ι be given.
Let x11 of type ι be given.
Let x12 of type ι be given.
Let x13 of type ι be given.
Let x14 of type ι be given.
Assume H2: x0 x2.
Assume H3: x0 x3.
Assume H4: x0 x4.
Assume H5: x0 x5.
Assume H6: x0 x6.
Assume H7: x0 x7.
Assume H8: x0 x8.
Assume H9: x0 x9.
Assume H10: x0 x10.
Assume H11: x0 x11.
Assume H12: x0 x12.
Assume H13: x0 x13.
Assume H14: x0 x14.
Apply unknownprop_cdf413c5f4dc1f383635da0ad98745a27213ad491b401aa0496ce6d27d593222 with
x0,
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x1 x11 x12,
x13,
x14,
λ x15 x16 . x16 = x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))) leaving 15 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
Apply H0 with
x11,
x12 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
set y15 to be ...
set y16 to be ...
Claim L15: ∀ x17 : ι → ο . x17 y16 ⟶ x17 y15
Let x17 of type ι → ο be given.
Assume H15: x17 (x3 x4 (x3 x5 (x3 x6 (x3 x7 (x3 x8 (x3 x9 (x3 x10 (x3 x11 (x3 x12 (x3 x13 (x3 x14 (x3 y15 y16)))))))))))).
set y18 to be ...
set y19 to be ...
set y20 to be ...
Claim L16: ∀ x21 : ι → ο . x21 y20 ⟶ x21 y19
Let x21 of type ι → ο be given.
Assume H16: x21 (x5 x7 (x5 x8 (x5 x9 (x5 x10 (x5 x11 (x5 x12 (x5 x13 (x5 x14 (x5 y15 (x5 y16 (x5 x17 y18))))))))))).
set y22 to be ...
set y23 to be ...
set y24 to be ...
Claim L17: ∀ x25 : ι → ο . x25 y24 ⟶ x25 y23
Let x25 of type ι → ο be given.
Assume H17: x25 (x7 x10 (x7 x11 (x7 x12 (x7 x13 (x7 x14 (x7 y15 (x7 ... ...))))))).
set y25 to be λ x25 x26 . y24 (x7 x9 x25) (x7 x9 x26)
Apply L17 with
λ x26 . y25 x26 y24 ⟶ y25 y24 x26 leaving 2 subgoals.
Assume H18: y25 y24 y24.
The subproof is completed by applying H18.
The subproof is completed by applying L17.
set y21 to be λ x21 x22 . y20 (x5 x6 x21) (x5 x6 x22)
Apply L16 with
λ x22 . y21 x22 y20 ⟶ y21 y20 x22 leaving 2 subgoals.
Assume H17: y21 y20 y20.
The subproof is completed by applying H17.
The subproof is completed by applying L16.
Let x17 of type ι → ι → ο be given.
Apply L15 with
λ x18 . x17 x18 y16 ⟶ x17 y16 x18.
Assume H16: x17 y16 y16.
The subproof is completed by applying H16.