Let x0 of type ι → ο be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι → ι → ι be given.
Assume H0: ∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4).
Assume H1: ∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x2 x3 x4).
Assume H2: ∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x1 x3 (x1 x4 x5) = x1 x4 (x1 x3 x5).
Assume H3: ∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x1 (x1 x3 x4) x5 = x1 x3 (x1 x4 x5).
Assume H4: ∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5).
Assume H5: ∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5).
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.
Assume H6: x0 x3.
Assume H7: x0 x4.
Assume H8: x0 x5.
Assume H9: x0 x6.
Assume H10: x0 x7.
set y8 to be ...
set y9 to be ...
Claim L11: ∀ x10 : ι → ο . x10 y9 ⟶ x10 y8
Let x10 of type ι → ο be given.
Assume H11: x10 (x3 (x4 x5 y8) (x3 (x4 x5 y9) (x3 (x4 x6 y8) (x3 (x4 x6 y9) (x3 (x4 x7 y8) (x4 x7 y9)))))).
Apply H4 with
x3 x5 (x3 x6 x7),
y8,
y9,
λ x11 . x10 leaving 4 subgoals.
Apply H0 with
x5,
x3 x6 x7 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H0 with
x6,
x7 leaving 2 subgoals.
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.
set y11 to be ...
set y12 to be ...
set y13 to be ...
Apply L12 with
λ x14 . y13 x14 y12 ⟶ y13 y12 x14 leaving 2 subgoals.
Assume H13: y13 y12 y12.
The subproof is completed by applying H13.
Apply unknownprop_15c431ceaba103d0f1b38ad69d2d9fb3fc0d806dc9533577ab3f7d79f4d15397 with
x5,
x6,
x7 y8 y11,
x7 y9 y11,
x7 x10 y11,
x7 y8 y12,
x7 y9 y12,
x7 x10 y12,
λ x14 x15 . x15 = x6 (x7 y8 y11) (x6 (x7 y8 y12) (x6 (x7 y9 y11) (x6 (x7 y9 y12) (x6 (x7 x10 y11) (x7 x10 y12))))),
λ x14 . y13 leaving 10 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Apply H2 with
y8,
y11 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H10.
Apply H2 with
y9,
y11 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H10.
Apply H2 with
x10,
y11 leaving 2 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
Apply H2 with
y8,
y12 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H11.
Apply H2 with
y9,
y12 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H11.
Apply H2 with
x10,
y12 leaving 2 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H11.
set y14 to be ...
set y15 to be ...
Let x16 of type ι → ι → ο be given.
Apply L13 with
λ x17 . x16 x17 y15 ⟶ x16 y15 x17.
Assume H14: x16 y15 ....
Let x10 of type ι → ι → ο be given.
Apply L11 with
λ x11 . x10 x11 y9 ⟶ x10 y9 x11.
Assume H12: x10 y9 y9.
The subproof is completed by applying H12.