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.
Assume H6: x0 x3.
Assume H7: x0 x4.
Assume H8: x0 x5.
Assume H9: x0 x6.
set y7 to be ...
set y8 to be ...
Claim L10: ∀ x9 : ι → ο . x9 y8 ⟶ x9 y7
Let x9 of type ι → ο be given.
Assume H10: x9 (x3 (x4 x5 y7) (x3 (x4 x5 y8) (x3 (x4 x6 y7) (x4 x6 y8)))).
Apply H4 with
x3 x5 x6,
y7,
y8,
λ x10 . x9 leaving 4 subgoals.
Apply H0 with
x5,
x6 leaving 2 subgoals.
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.
set y10 to be ...
set y11 to be ...
set y12 to be ...
Apply L11 with
λ x13 . y12 x13 y11 ⟶ y12 y11 x13 leaving 2 subgoals.
Assume H12: y12 y11 y11.
The subproof is completed by applying H12.
Apply unknownprop_4aef431da355638d092d1af3952763e46a0de88399b3400cacc13c5390d4cf48 with
x5,
x6,
y7 y8 y10,
y7 x9 y10,
y7 y8 y11,
y7 x9 y11,
λ x13 x14 . x14 = x6 (y7 y8 y10) (x6 (y7 y8 y11) (x6 (y7 x9 y10) (y7 x9 y11))),
λ x13 . y12 leaving 8 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Apply H2 with
y8,
y10 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
Apply H2 with
x9,
y10 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
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
x9,
y11 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H10.
set y13 to be ...
set y14 to be ...
Claim L12: ∀ x15 : ι → ο . x15 y14 ⟶ x15 y13
Let x15 of type ι → ο be given.
Assume H12: x15 (y8 (x9 y10 y12) (y8 (x9 y10 y13) (y8 (x9 y11 y12) (x9 y11 y13)))).
set y16 to be ...
Apply H3 with
x9 y11 y12,
x9 y10 y13,
x9 y11 y13,
λ x17 x18 . y16 (y8 ... ...) ... leaving 4 subgoals.
Let x15 of type ι → ι → ο be given.
Apply L12 with
λ x16 . x15 x16 y14 ⟶ x15 y14 x16.
Assume H13: x15 y14 y14.
The subproof is completed by applying H13.
Let x9 of type ι → ι → ο be given.
Apply L10 with
λ x10 . x9 x10 y8 ⟶ x9 y8 x10.
Assume H11: x9 y8 y8.
The subproof is completed by applying H11.