th 16.2 proved in the setoids setting

[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 9fd5b7eeb77c78d77de0fb5b220f42e93f84779d..5600b9a16a49ed4fc7992de19a5fed5de94dba0f 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -123,17 +123,18 @@ nlemma mem_ext_powerclass_setoid_is_morph:
   [ napply (. (ext_prop … Ha^-1)) | napply (. (ext_prop … Ha)) ] /2/.
 nqed.
 
-unification hint 0 ≔  A:setoid, x, S;  
+unification hint 0 ≔  AA, x, S;  
+     A ≟ carr AA,
      SS ≟ (ext_carr ? S),
      TT ≟ (mk_unary_morphism1 … 
              (λx:setoid1_of_setoid ?.
                mk_unary_morphism1 …
                  (λS:ext_powerclass_setoid ?. x ∈ S)
-                 (prop11 … (mem_ext_powerclass_setoid_is_morph A x)))
-             (prop11 … (mem_ext_powerclass_setoid_is_morph A))),
-     XX ≟ (ext_powerclass_setoid A)
+                 (prop11 … (mem_ext_powerclass_setoid_is_morph AA x)))
+             (prop11 … (mem_ext_powerclass_setoid_is_morph AA))),
+     XX ≟ (ext_powerclass_setoid AA)
   (*-------------------------------------*) ⊢ 
-      fun11 (setoid1_of_setoid A)
+      fun11 (setoid1_of_setoid AA)
        (unary_morphism1_setoid1 XX CPROP) TT x S 
     ≡ mem A SS x.
 
@@ -143,6 +144,7 @@ nlemma subseteq_is_morph: ∀A. unary_morphism1 (ext_powerclass_setoid A)
  #a; #a'; #b; #b'; *; #H1; #H2; *; /5/ by mk_iff, sym1, subseteq_trans;
 nqed.
 
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type2".
 unification hint 0 ≔ A,a,a'
  (*-----------------------------------------------------------------*) ⊢
   eq_rel ? (eq0 A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'.
@@ -189,18 +191,19 @@ nlemma intersect_is_ext_morph:
 nqed.
 
 unification hint 1 ≔ 
-      A:setoid, B,C : 𝛀^A;
+      AA : setoid, B,C : 𝛀^AA;
+      A ≟ carr AA,
       R ≟ (mk_unary_morphism1 …
-              (λS:ext_powerclass_setoid A.
+              (λS:ext_powerclass_setoid AA.
                mk_unary_morphism1 ??
-                (λS':ext_powerclass_setoid A.
-                  mk_ext_powerclass A (S∩S') (ext_prop A (intersect_is_ext ? S S')))
-                (prop11 … (intersect_is_ext_morph A S))) 
-              (prop11 … (intersect_is_ext_morph A))) ,
+                (λS':ext_powerclass_setoid AA.
+                  mk_ext_powerclass AA (S∩S') (ext_prop AA (intersect_is_ext ? S S')))
+                (prop11 … (intersect_is_ext_morph AA S))) 
+              (prop11 … (intersect_is_ext_morph AA))) ,
        BB ≟ (ext_carr ? B),
        CC ≟ (ext_carr ? C)
    (* ------------------------------------------------------*) ⊢ 
-            ext_carr A (R B C) ≡ intersect (carr A) BB CC.
+            ext_carr AA (R B C) ≡ intersect A BB CC.
 
 (*
 alias symbol "hint_decl" = "hint_decl_Type2".