(* carr1 e' necessario perche' ci sega via la coercion per gli oggetti di REL!
(confondendola con la coercion per gli oggetti di SET
record concrete_space : Type[1] ≝
(* carr1 e' necessario perche' ci sega via la coercion per gli oggetti di REL!
(confondendola con la coercion per gli oggetti di SET
record concrete_space : Type[1] ≝