| λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . λ x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (and (and (MetaCat_terminal_p x0 x1 x2 x3 x4 x5) (x0 x6)) (x1 x4 x6 x7)) (x1 x6 x6 x8)) (∀ x10 x11 x12 . x0 x10 ⟶ x1 x4 x10 x11 ⟶ x1 x10 x10 x12 ⟶ and (and (and (x1 x6 x10 (x9 x10 x11 x12)) (x3 x4 x6 x10 (x9 x10 x11 x12) x7 = x11)) (x3 x6 x6 x10 (x9 x10 x11 x12) x8 = x3 x6 x10 x10 x12 (x9 x10 x11 x12))) (∀ x13 . x1 x6 x10 x13 ⟶ x3 x4 x6 x10 x13 x7 = x11 ⟶ x3 x6 x6 x10 x13 x8 = x3 x6 x10 x10 x12 x13 ⟶ x13 = x9 x10 x11 x12)) |
|