(* subset less or equal (inclusion) *)
definition sle: \forall D. Subset D \to Subset D \to Prop \def
- \lambda D,U1,U2. \forall d. U1 d \to U2 d.
-(*
+ \lambda D,U1,U2. \iforall d. U1 d \to U2 d.
+
(* subset overlap *)
definition sover: \forall D. Subset D \to Subset D \to Prop \def
- \lambda D,U1,U2. \forall d. U1 d \to U2 d.
-*)
+ \lambda D,U1,U2. \iexists d. U1 d \land U2 d.
(* 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 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
\lambda (D:Domain). \lambda U.
mk_Domain (mk_Class D (sin D U) (cle1 D)).
-coercion domain_of_subset.
-
(* the full subset of a domain *)
coercion stop.
-