some definitions about subsets

[helm.git] / helm / matita / contribs / PREDICATIVE-TOPOLOGY / domain_defs.ma

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
index 821002e685bc63533fa5aeb7b1066a59e59cd8b3..670211caf3cee1f047c44187a6f222f9fbc13ae6 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
@@ -23,20 +23,22 @@ include "class_defs.ma".
      domain structure. This makes domains easier to use
 *)
 
-
-
 record Domain: Type \def {
    qd: Class
 }.
 
 coercion qd.
 
-
-
 (* internal universal quantification *)
 inductive iall (D:Domain) (P:D \to Prop) : Prop \def
    | iall_intro: (\forall d:D. cin D d \to P d) \to iall D P.
 
+(* internal existential quantification *)
+inductive iex (D:Domain) (P:D \to Prop) : Prop \def
+   | iex_intro: \forall d:D. cin D d \land P d \to iex D P.
+(*
+(* notations **************************************************************)
+
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "internal for all" 'iall \eta.x =
   (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/iall.ind#xpointer(1/1) _ x).
@@ -47,12 +49,6 @@ for @{ 'iall ${default
   @{\lambda ${ident i} : $ty. $p)}
   @{\lambda ${ident i} . $p}}}.
 
-
-
-(* internal existential quantification *)
-inductive iex (D:Domain) (P:D \to Prop) : Prop \def
-   | iex_intro: \forall d:D. cin D d \land P d \to iex D P.
-
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "internal exist" 'iexist \eta.x =
   (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/iex.ind#xpointer(1/1) _ x).
@@ -62,3 +58,4 @@ notation < "hvbox(\iexist ident i opt (: ty) break . p)"
 for @{ 'iexist ${default
   @{\lambda ${ident i} : $ty. $p)}
   @{\lambda ${ident i} . $p}}}.
+*)
\ No newline at end of file