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