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