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.
Let x15 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.
Assume H15: x0 x15.
Apply unknownprop_f054fae7c9dd7e6cce73b44372104a53926f15847132949a5b6f3599c61d6044 with
x0,
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x1 x12 x13,
x14,
x15,
λ x16 x17 . x17 = x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))))))))) leaving 16 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.
The subproof is completed by applying H11.
Apply H0 with
x12,
x13 leaving 2 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H15.
set y16 to be ...
set y17 to be ...
Claim L16: ∀ x18 : ι → ο . x18 y17 ⟶ x18 y16
Let x18 of type ι → ο be given.
Assume H16: x18 (x3 x4 (x3 x5 (x3 x6 (x3 x7 (x3 x8 (x3 x9 (x3 x10 (x3 x11 (x3 x12 (x3 x13 (x3 x14 (x3 x15 (x3 y16 y17))))))))))))).
set y19 to be ...
set y20 to be ...
set y21 to be ...
Claim L17: ∀ x22 : ι → ο . x22 y21 ⟶ x22 y20
Let x22 of type ι → ο be given.
Assume H17: x22 (x5 x7 (x5 x8 (x5 x9 (x5 x10 (x5 x11 (x5 x12 (x5 x13 (x5 x14 (x5 x15 (x5 y16 (x5 y17 (x5 x18 y19)))))))))))).
set y23 to be ...
set y24 to be ...
set y25 to be ...
Claim L18: ∀ x26 : ι → ο . x26 y25 ⟶ x26 y24
Let x26 of type ι → ο be given.
Assume H18: x26 (x7 x10 (x7 ... ...)).
set y26 to be λ x26 x27 . y25 (x7 x9 x26) (x7 x9 x27)
Apply L18 with
λ x27 . y26 x27 y25 ⟶ y26 y25 x27 leaving 2 subgoals.
Assume H19: y26 y25 y25.
The subproof is completed by applying H19.
The subproof is completed by applying L18.
set y22 to be λ x22 x23 . y21 (x5 x6 x22) (x5 x6 x23)
Apply L17 with
λ x23 . y22 x23 y21 ⟶ y22 y21 x23 leaving 2 subgoals.
Assume H18: y22 y21 y21.
The subproof is completed by applying H18.
The subproof is completed by applying L17.
Let x18 of type ι → ι → ο be given.
Apply L16 with
λ x19 . x18 x19 y17 ⟶ x18 y17 x19.
Assume H17: x18 y17 y17.
The subproof is completed by applying H17.