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.
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.
Apply unknownprop_a3dc646a3957ef41aa3900f732ba2cb2ede42a23cf46d988ba85bc5ae48c040a with
x0,
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x1 x8 x9,
x10,
x11,
λ x12 x13 . x13 = x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))))) leaving 12 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.
Apply H0 with
x8,
x9 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
set y12 to be ...
set y13 to be ...
Claim L12: ∀ x14 : ι → ο . x14 y13 ⟶ x14 y12
Let x14 of type ι → ο be given.
Assume H12: x14 (x3 x4 (x3 x5 (x3 x6 (x3 x7 (x3 x8 (x3 x9 (x3 x10 (x3 x11 (x3 y12 y13))))))))).
set y15 to be ...
set y16 to be ...
set y17 to be ...
Claim L13: ∀ x18 : ι → ο . x18 y17 ⟶ x18 y16
Let x18 of type ι → ο be given.
Assume H13: x18 (x5 x7 (x5 x8 (x5 x9 (x5 x10 (x5 x11 (x5 y12 (x5 y13 (x5 x14 y15)))))))).
set y19 to be ...
set y20 to be ...
set y21 to be ...
Claim L14: ∀ x22 : ι → ο . x22 y21 ⟶ x22 y20
Let x22 of type ι → ο be given.
Assume H14: x22 (x7 x10 (x7 x11 (x7 y12 (x7 y13 (x7 x14 (x7 y15 (x7 y16 y17))))))).
set y23 to be ...
set y24 to be ...
set y25 to be ...
Claim L15: ∀ x26 : ι → ο . x26 y25 ⟶ x26 y24
Let x26 of type ι → ο be given.
Assume H15: x26 ....
set y26 to be λ x26 x27 . y25 (x9 y12 x26) (x9 y12 x27)
Apply L15 with
λ x27 . y26 x27 y25 ⟶ y26 y25 x27 leaving 2 subgoals.
Assume H16: y26 y25 y25.
The subproof is completed by applying H16.
The subproof is completed by applying L15.
set y22 to be λ x22 x23 . y21 (x7 x9 x22) (x7 x9 x23)
Apply L14 with
λ x23 . y22 x23 y21 ⟶ y22 y21 x23 leaving 2 subgoals.
Assume H15: y22 y21 y21.
The subproof is completed by applying H15.
The subproof is completed by applying L14.
set y18 to be λ x18 x19 . y17 (x5 x6 x18) (x5 x6 x19)
Apply L13 with
λ x19 . y18 x19 y17 ⟶ y18 y17 x19 leaving 2 subgoals.
Assume H14: y18 y17 y17.
The subproof is completed by applying H14.
The subproof is completed by applying L13.
Let x14 of type ι → ι → ο be given.
Apply L12 with
λ x15 . x14 x15 y13 ⟶ x14 y13 x15.
Assume H13: x14 y13 y13.
The subproof is completed by applying H13.