(confondendola con la coercion per gli oggetti di SET *)
record concrete_space : Type1 ≝
{ bp:> BP;
- converges: ∀a: carr1 (concr bp).∀U,V: carr1 (form bp). a ⊩ U → a ⊩ V → a ⊩_bp (U ↓ V);
+ 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
}.