nicer hints, 16.1->3 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 d547fbbbfcbd37efadd825e130a9575b3e6d892a..0038ad4f652bcea45dcc2e2866fd191d6fe2bc77 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -185,6 +185,7 @@ nqed.
 unification hint 1 ≔ 
       AA : setoid, B,C : 𝛀^AA;
       A ≟ carr AA,
+      T ≟ ext_powerclass_setoid AA,
       R ≟ (mk_unary_morphism1 ??
               (λS:𝛀^AA.
                mk_unary_morphism1 ??
@@ -194,11 +195,11 @@ unification hint 1 ≔
               (prop11 ?? (intersect_is_ext_morph AA))) ,
        BB ≟ (ext_carr ? B),
        CC ≟ (ext_carr ? C)
-   (* ------------------------------------------------------*) ⊢ 
-            ext_carr AA (R B C) ≡ intersect A BB CC.
+   (* ---------------------------------------------------------------------------------------*) ⊢ 
+      ext_carr AA (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ intersect A BB CC.
 
 
-(* hints for â\88© *)
+(* hints for â\88ª *)
 nlemma union_is_morph : ∀A. Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
 #X; napply (mk_binary_morphism1 … (λA,B.A ∪ B));
 #A1 A2 B1 B2 EA EB; napply ext_set; #x;
@@ -238,6 +239,7 @@ nqed.
 unification hint 1 ≔
   AA : setoid, B,C : 𝛀^AA;
   A ≟ carr AA,
+  T ≟ ext_powerclass_setoid AA,  
   R ≟ (mk_unary_morphism1 ??
           (λS:𝛀^AA.
            mk_unary_morphism1 ??
@@ -248,7 +250,7 @@ unification hint 1 ≔
    BB ≟ (ext_carr ? B),
    CC ≟ (ext_carr ? C)
 (*------------------------------------------------------*) ⊢
-   ext_carr AA (R B C) ≡ union A BB CC.
+   ext_carr AA (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ union A BB CC.
 
 
 (* hints for - *)
@@ -288,6 +290,7 @@ nqed.
 unification hint 1 ≔
   AA : setoid, B,C : 𝛀^AA;
   A ≟ carr AA,
+  T ≟ ext_powerclass_setoid AA,    
   R ≟ (mk_unary_morphism1 ??
           (λS:𝛀^AA.
            mk_unary_morphism1 ??
@@ -298,7 +301,7 @@ unification hint 1 ≔
    BB ≟ (ext_carr ? B),
    CC ≟ (ext_carr ? C)
 (*------------------------------------------------------*) ⊢
-   ext_carr AA (R B C) ≡ substract A BB CC.
+   ext_carr AA (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ substract A BB CC.
 
 (* hints for {x} *)
 nlemma single_is_morph : ∀A:setoid. (setoid1_of_setoid A) ⇒_1 Ω^A.
@@ -316,22 +319,24 @@ unification hint 0 ≔ A : setoid, a:A;
 
 unification hint 0 ≔ A:setoid, a:A;
   T ≟ setoid1_of_setoid A,
+  AA ≟ carr A,
   MM ≟ mk_unary_morphism1 ?? 
          (λa:setoid1_of_setoid A.{(a)}) (prop11 ?? (single_is_morph A))
 (*--------------------------------------------------------------------------*) ⊢
-   fun11 T (powerclass_setoid A) MM a ≡ {(a)}.
+   fun11 T (powerclass_setoid AA) 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.
             
 unification hint 1 ≔
   AA : setoid, a: AA;
+  T ≟ ext_powerclass_setoid AA,
   R ≟ mk_unary_morphism1 ??
        (λa:setoid1_of_setoid AA.
          mk_ext_powerclass AA {(a)} (ext_prop ? (single_is_ext AA a)))
             (prop11 ?? (single_is_ext_morph AA))
 (*------------------------------------------------------*) ⊢
-   ext_carr AA (R a) ≡ singleton AA a.
+   ext_carr AA (fun11 (setoid1_of_setoid AA) T R a) ≡ singleton AA a.