| ∀ x0 : ι → ο . (∀ x1 : (ι → ο) → ο . (∀ x2 : ι → ο . x1 x2 ⟶ x1 (λ x3 . and (x2 x3) (x3 = prim0 x2 ⟶ ∀ x4 : ο . x4))) ⟶ (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x1 x3) ⟶ x1 (Descr_Vo1 x2)) ⟶ x1 x0) ⟶ ∀ x1 : (ι → ο) → ο . (∀ x2 : ι → ο . x1 x2 ⟶ x1 (λ x3 . and (x2 x3) (x3 = prim0 x2 ⟶ ∀ x4 : ο . x4))) ⟶ (∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x1 x3) ⟶ x1 (Descr_Vo1 x2)) ⟶ x1 (λ x2 . and (x0 x2) (x2 = prim0 x0 ⟶ ∀ x3 : ο . x3)) |
|