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 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5).
Assume H2: ∀ 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.
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.
Let x16 of type ι be given.
Let x17 of type ι be given.
Let x18 of type ι be given.
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.
Assume H16: x0 x16.
Assume H17: x0 x17.
Assume H18: x0 x18.
Apply unknownprop_96890bb6437669c5e09c9ab608ee6937f060bce73200a8371786914ccb14f8e2 with
x0,
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 (x1 x17 x18)))))),
λ x19 x20 . x20 = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x1 (x2 x3 x16) (x1 (x2 x3 x17) (x2 x3 x18)))))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x1 (x2 x4 x16) (x1 (x2 x4 x17) (x2 x4 x18)))))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x1 (x2 x5 x16) (x1 (x2 x5 x17) (x2 x5 x18)))))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x1 (x2 x6 x16) (x1 (x2 x6 x17) (x2 x6 x18)))))))) (x1 ... ...)))) leaving 12 subgoals.