- converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
- all_covered: ∀x: concr bp. x ⊩ full_subset (form bp)
+ converges: ∀a: carr1 (concr bp).∀U,V: carr1 (form bp). a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
+ all_covered: ∀x: carr1 (concr bp). x ⊩ form bp