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