(* 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 full subset of a domain *)
coercion stop.
-