many fixes to setoids for re, 16.1 almost done

[helm.git] / helm / software / matita / nlibrary / sets / sets.ma

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index aae969ed208f25ba2eab0cd1b3efa4cc78217372..d547fbbbfcbd37efadd825e130a9575b3e6d892a 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -148,7 +148,7 @@ nqed.
 (* hints for ∩ *)
 nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
 #S A B; @ (A ∩ B); #x y Exy; @; *; #H1 H2; @;
-##[##1,2: napply (. Exy^-1â\80¡#); nassumption;
+##[##1,2: napply (. Exy^-1â\95ª_1#); nassumption;
 ##|##3,4: napply (. Exy‡#); nassumption]
 nqed.
 
@@ -166,11 +166,12 @@ nqed.
 
 alias symbol "hint_decl" = "hint_decl_Type1".
 unification hint 0 ≔ A : Type[0], B,C : Ω^A;
+  T ≟ powerclass_setoid A,
   R ≟ mk_unary_morphism1 ??
        (λS. mk_unary_morphism1 ?? (λS'.S ∩ S') (prop11 ?? (intersect_is_morph A S))) 
        (prop11 ?? (intersect_is_morph A))
 (*------------------------------------------------------------------------*) ⊢ 
-    fun11 ?? (fun11 ?? R B) C  ≡ intersect A B C.
+    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C  ≡ intersect A B C.
 
 interpretation "prop21 ext" 'prop2 l r =
  (prop11 (ext_powerclass_setoid ?)
@@ -222,11 +223,12 @@ unification hint 0 ≔
     ext_carr A R ≡ union ? (ext_carr ? B) (ext_carr ? C).
 
 unification hint 0 ≔ S:Type[0], A,B:Ω^S;
+  T ≟ powerclass_setoid S,
   MM ≟ mk_unary_morphism1 ??
         (λA.mk_unary_morphism1 ?? (λB.A ∪ B) (prop11 ?? (union_is_morph S A)))
         (prop11 ?? (union_is_morph S))
 (*--------------------------------------------------------------------------*) ⊢
-   fun11 ?? (fun11 ?? MM A) B ≡ A ∪ B.
+   fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A ∪ B.
    
 nlemma union_is_ext_morph:∀A.𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A.
 #A; napply (mk_binary_morphism1 …  (union_is_ext …));
@@ -271,11 +273,12 @@ unification hint 0 ≔
     ext_carr A R ≡ substract ? (ext_carr ? B) (ext_carr ? C).
 
 unification hint 0 ≔ S:Type[0], A,B:Ω^S;
+  T ≟ powerclass_setoid S,  
   MM ≟ mk_unary_morphism1 ??
         (λA.mk_unary_morphism1 ?? (λB.A - B) (prop11 ?? (substract_is_morph S A)))
         (prop11 ?? (substract_is_morph S))
 (*--------------------------------------------------------------------------*) ⊢
-   fun11 ?? (fun11 ?? MM A) B ≡ A - B.
+   fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A - B.
    
 nlemma substract_is_ext_morph:∀A.𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A.
 #A; napply (mk_binary_morphism1 …  (substract_is_ext …));
@@ -312,10 +315,11 @@ unification hint 0 ≔ A : setoid, a:A;
     ext_carr A R ≡ singleton A a.
 
 unification hint 0 ≔ A:setoid, a:A;
+  T ≟ setoid1_of_setoid A,
   MM ≟ mk_unary_morphism1 ?? 
          (λa:setoid1_of_setoid A.{(a)}) (prop11 ?? (single_is_morph A))
 (*--------------------------------------------------------------------------*) ⊢
-   fun11 ?? MM a ≡ {(a)}.
+   fun11 T (powerclass_setoid A) MM a ≡ {(a)}.
    
 nlemma single_is_ext_morph:∀A:setoid.(setoid1_of_setoid A) ⇒_1 𝛀^A.
 #A; @; ##[ #a; napply (single_is_ext ? a); ##] #a b E; @; #x; /3/; nqed.