-(* coercions **************************************************************)
-
-(*
-(* 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 *)
+definition subsets_of_domain ≝
+ λD. mk_Class (Subset D) (true_f ?) (sle ?).