(* the class of the subsets of a domain (not an implicit coercion) *)
definition class_of_subsets_of \def
\lambda D. mk_Class (Subset D) (true_f ?) (sle ?).
(* the class of the subsets of a domain (not an implicit coercion) *)
definition class_of_subsets_of \def
\lambda D. mk_Class (Subset D) (true_f ?) (sle ?).
-(* the domain built upon a subset *)
-definition domain_of_subset: \forall D. (Subset D) \to Domain \def
+(* the domain built upon a subset (not an implicit coercion) *)
+definition domain_of_subset: \forall D. Subset D \to Domain \def