| ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ι → ι . ∀ x6 x7 : ι → ι . MetaMonad x0 x1 x2 x3 x4 x5 x6 x7 ⟶ ∀ x8 : ο . ((∀ x9 . x0 x9 ⟶ x3 (x4 (x4 (x4 x9))) (x4 (x4 x9)) (x4 x9) (x7 x9) (x5 (x4 (x4 x9)) (x4 x9) (x7 x9)) = x3 (x4 (x4 (x4 x9))) (x4 (x4 x9)) (x4 x9) (x7 x9) (x7 (x4 x9))) ⟶ (∀ x9 . x0 x9 ⟶ x3 (x4 x9) (x4 (x4 x9)) (x4 x9) (x7 x9) (x6 (x4 x9)) = x2 (x4 x9)) ⟶ (∀ x9 . x0 x9 ⟶ x3 (x4 x9) (x4 (x4 x9)) (x4 x9) (x7 x9) (x5 x9 (x4 x9) (x6 x9)) = x2 (x4 x9)) ⟶ x8) ⟶ x8 |
|