| ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 x15 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))) = x1 (x2 x15 x3) (x1 (x2 x15 x4) (x1 (x2 x15 x5) (x1 (x2 x15 x6) (x1 (x2 x15 x7) (x1 (x2 x15 x8) (x1 (x2 x15 x9) (x1 (x2 x15 x10) (x1 (x2 x15 x11) (x1 (x2 x15 x12) (x1 (x2 x15 x13) (x2 x15 x14))))))))))) |
|