| ∀ 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 x16 . 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 ⟶ x0 x16 ⟶ x2 x16 (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)))))))))))) = x1 (x2 x16 x3) (x1 (x2 x16 x4) (x1 (x2 x16 x5) (x1 (x2 x16 x6) (x1 (x2 x16 x7) (x1 (x2 x16 x8) (x1 (x2 x16 x9) (x1 (x2 x16 x10) (x1 (x2 x16 x11) (x1 (x2 x16 x12) (x1 (x2 x16 x13) (x1 (x2 x16 x14) (x2 x16 x15)))))))))))) |
|