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