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