From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Sep 2010 23:09:45 +0000 (+0000)
Subject: hints polished and fixed to allow recursive inference of ext_carr
X-Git-Tag: make_still_working~2820
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d1c9cdb2de96aa2dda6a7b25a4c4959b82b08f6c;p=helm.git

hints polished and fixed to allow recursive inference of ext_carr
---

diff --git a/helm/software/matita/nlibrary/datatypes/list-setoids.ma b/helm/software/matita/nlibrary/datatypes/list-setoids.ma
index c836f4bf3..6a1532562 100644
--- a/helm/software/matita/nlibrary/datatypes/list-setoids.ma
+++ b/helm/software/matita/nlibrary/datatypes/list-setoids.ma
@@ -36,13 +36,13 @@ unification hint 0 ≔ S : setoid;
   P1 ≟ refl ? (eq0 (LIST S)),
   P2 ≟ sym ? (eq0 (LIST S)),
   P3 ≟ trans ? (eq0 (LIST S)),
-  X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list T) P1 P2 P3)
+  X ≟ mk_setoid (list (carr S)) (mk_equivalence_relation ? (eq_list S) P1 P2 P3)
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ list T.
 
-unification hint 0 ≔ S:setoid,a,b:list S;
+unification hint 0 ≔ S:setoid, a,b:list (carr S);
    R ≟ eq0 (LIST S),
-   L ≟ (list S)
+   L ≟ (list (carr S))
 (* -------------------------------------------- *) ⊢
    eq_list S a b ≡ eq_rel L R a b.
 
@@ -53,13 +53,15 @@ nlemma append_is_morph : ∀A:setoid.(list A) ⇒_0 (list A) ⇒_0 (list A).
 nqed.
 
 alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
-unification hint 0 ≔ S:setoid, A,B:list S;
-    MM ≟ mk_unary_morphism ??
-          (λA:list S.mk_unary_morphism ?? (λB:list S.A @ B) (prop1 ?? (append_is_morph S A)))
+unification hint 0 ≔ S:setoid, A,B:list (carr S);
+    SS ≟ carr S,
+    MM ≟ mk_unary_morphism ?? (λA:list (carr S).
+            mk_unary_morphism ?? 
+              (λB:list (carr S).A @ B) (prop1 ?? (fun1 ??(append_is_morph S) A)))
           (prop1 ?? (append_is_morph S)),
     T ≟ LIST S
 (*--------------------------------------------------------------------------*) ⊢
-   fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ A @ B.
+   fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ append SS A B.
 
 
 (* XXX to understand if are always needed or only if the coercion is active *)
diff --git a/helm/software/matita/nlibrary/datatypes/pairs-setoids.ma b/helm/software/matita/nlibrary/datatypes/pairs-setoids.ma
index 43c12f768..f68305720 100644
--- a/helm/software/matita/nlibrary/datatypes/pairs-setoids.ma
+++ b/helm/software/matita/nlibrary/datatypes/pairs-setoids.ma
@@ -42,7 +42,7 @@ unification hint 0 ≔ AA, BB;
  
 unification hint 0 ≔ S1,S2,a,b;
    R ≟ PAIR S1 S2,
-   L ≟ (pair S1 S2)
+   L ≟ pair (carr S1) (carr S2)
 (* -------------------------------------------- *) ⊢
    eq_pair S1 S2 a b ≡ eq_rel L (eq0 R) a b.    
 
diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index 9b352d4a4..e7ecf01ad 100644
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -50,9 +50,9 @@ nqed.
 
 unification hint 0 ≔ A,B:CProp[0];
   T ≟ CPROP,
-  MM ≟ mk_unary_morphism1 …
-       (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
-         (prop11 … and_morphism)
+  MM ≟ mk_unary_morphism1 ??
+       (λX.mk_unary_morphism1 ?? (And X) (prop11 ?? (fun11 ?? and_morphism X)))
+         (prop11 ?? and_morphism)
 (*-------------------------------------------------------------*) ⊢
   fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ And A B.
 
@@ -76,7 +76,7 @@ nqed.
 unification hint 0 ≔ A,B:CProp[0];
   T ≟ CPROP,
   MM ≟ mk_unary_morphism1 …
-       (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
+       (λX.mk_unary_morphism1 … (Or X) (prop11 … (fun11 ?? or_morphism X)))
          (prop11 … or_morphism)
 (*-------------------------------------------------------------*) ⊢
   fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ Or A B.
@@ -121,33 +121,35 @@ nlemma Ex_morphism : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CP
 #S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P); 
 #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
 
-unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CProp[0];
+unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CPROP;
    A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP, 
    B ≟ CPROP,
-   M ≟ mk_unary_morphism1 ?? (λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P) 
-        (prop11 ?? (Ex_morphism S))
+   M ≟ mk_unary_morphism1 ?? 
+         (λP: (setoid1_of_setoid S) ⇒_1 CPROP.Ex (carr S) (fun11 ?? P)) 
+         (prop11 ?? (Ex_morphism S))
 (*------------------------*)⊢
-  fun11 A B M P ≡ Ex S (fun11 (setoid1_of_setoid S) CPROP P).
+  fun11 A B M P ≡ Ex (carr S) (fun11 (setoid1_of_setoid S) CPROP P).
 
 nlemma Ex_morphism_eta : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
 #S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S (λx.P x)); 
 #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
 
-unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CProp[0];
+unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CPROP;
    A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP, 
    B ≟ CPROP,
-   M ≟ mk_unary_morphism1 ?? (λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S (λx.P x)) 
-        (prop11 ?? (Ex_morphism_eta S))
+   M ≟ mk_unary_morphism1 ?? 
+         (λP: (setoid1_of_setoid S) ⇒_1 CPROP.Ex (carr S) (λx.fun11 ?? P x)) 
+         (prop11 ?? (Ex_morphism_eta S))
 (*------------------------*)⊢
-  fun11 A B M P ≡ Ex S (λx.fun11 (setoid1_of_setoid S) CPROP P x).
+  fun11 A B M P ≡ Ex (carr S) (λx.fun11 (setoid1_of_setoid S) CPROP P x).
 
 nlemma Ex_setoid : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CPROP) → setoid.
 #T P; @ (Ex T (λx:T.P x)); @; ##[ #H1 H2; napply True |##*: //; ##] nqed.
 
-unification hint 0 ≔ T,P ; 
+unification hint 0 ≔ T : setoid,P ; 
    S ≟ (Ex_setoid T P) 
 (*---------------------------*) ⊢
-   Ex T (λx:T.P x) ≡ carr S.
+   Ex (carr T) (λx:carr T.fun11 ?? P x) ≡ carr S.
 
 (* couts how many Ex we are traversing *)
 ninductive counter : Type[0] ≝ 
diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index cfbd7cb31..47295f3fd 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -114,7 +114,7 @@ notation "0" non associative with precedence 90 for @{ 'empty_r }.
 interpretation "empty" 'empty_r = (z ?).
 
 notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }.
-notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }.
+notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(LIST $S) }.
  
 (* setoid support for re *)
  
@@ -156,9 +156,9 @@ unification hint 0 ≔ A : Alpha;
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ re T.
 
-unification hint 0 ≔ A:Alpha,a,b:re A;
+unification hint 0 ≔ A:Alpha, a,b:re (carr (acarr A));
    R ≟ eq0 (RE A),
-   L ≟ re A
+   L ≟ re (carr (acarr A))
 (* -------------------------------------------- *) ⊢
    eq_re A a b ≡ eq_rel L R a b.
 
@@ -173,13 +173,15 @@ nqed.
 
 (* XXX This is the good format for hints about morphisms, fix the others *)
 alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
-unification hint 0 ≔ S:Alpha, A,B:re S;
-    MM ≟ mk_unary_morphism ??
-          (λA:re S.mk_unary_morphism ?? (λB.A · B) (prop1 ?? (c_is_morph S A)))
-          (prop1 ?? (c_is_morph S)),
+unification hint 0 ≔ S:Alpha, A,B:re (carr (acarr S));
+    SS ≟ carr (acarr S),
+    MM ≟ mk_unary_morphism ?? (λA.
+           mk_unary_morphism ?? 
+             (λB.A · B) (prop1 ?? (fun1 ?? (c_is_morph S) A)))
+           (prop1 ?? (c_is_morph S)),
     T ≟ RE S
 (*--------------------------------------------------------------------------*) ⊢
-   fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ A · B.
+   fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ c SS A B.
 
 nlemma o_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A) ⇒_0 (re A).
 #A; napply (mk_binary_morphism … (λs1,s2:re A. s1 + s2));
@@ -190,13 +192,15 @@ nlemma o_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A) ⇒_0 (re A).
 ##|#r IH a'; ncases a'; nnormalize; /2/ by conj; ##]
 nqed.
 
-unification hint 0 ≔ S:Alpha, A,B:re S;
-    MM ≟ mk_unary_morphism ??
-          (λA:re S.mk_unary_morphism ?? (λB.A + B) (prop1 ?? (o_is_morph S A)))
-          (prop1 ?? (o_is_morph S)),
+unification hint 0 ≔ S:Alpha, A,B:re (carr (acarr S));
+    SS ≟ carr (acarr S),
+    MM ≟ mk_unary_morphism ?? (λA.
+           mk_unary_morphism ?? 
+             (λB.A + B) (prop1 ?? (fun1 ?? (o_is_morph S) A)))
+           (prop1 ?? (o_is_morph S)),
     T ≟ RE S
 (*--------------------------------------------------------------------------*) ⊢
-   fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ A + B.
+   fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ o SS A B.
 
 (* end setoids support for re *)
 
@@ -233,19 +237,23 @@ ncut (∀w1,w2.(x == w1@w2) = (y == w1@w2)); ##[
 nqed.
 
 alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔ A : setoid, B,C :  Elang A;
+unification hint 0 ≔ A : setoid, B,C : Elang A;
    AA ≟ LIST A,
-   R ≟ mk_ext_powerclass ? 
-         (ext_carr ? B · ext_carr ? C) (ext_prop ? (cat_is_ext ? B C))
-(*--------------------------------------------------------------------*)  ⊢
-    ext_carr AA R ≡ cat A (ext_carr AA B) (ext_carr AA C).
+   BB ≟ ext_carr AA B,
+   CC ≟ ext_carr AA C,
+   R ≟ mk_ext_powerclass AA
+         (cat A (ext_carr AA B) (ext_carr AA C)) 
+         (ext_prop AA (cat_is_ext A B C))
+(*----------------------------------------------------------*)  ⊢
+    ext_carr AA R ≡ cat A BB CC.
     
-unification hint 0 ≔ S:setoid, A,B:lang S;
-    T ≟ powerclass_setoid (list S),
+unification hint 0 ≔ S:setoid, A,B:lang (carr S);
+    T ≟ powerclass_setoid (list (carr S)),
     MM ≟ mk_unary_morphism1 T (unary_morphism1_setoid1 T T)
-          (λA:lang S.
+          (λA:lang (carr S).
              mk_unary_morphism1 T T 
-               (λB:lang S.cat S A B) (prop11 T T (cat_is_morph S A)))
+               (λB:lang (carr S).cat S A B) 
+               (prop11 T T (fun11 ?? (cat_is_morph S) A)))
           (prop11 T (unary_morphism1_setoid1 T T) (cat_is_morph S))
 (*--------------------------------------------------------------------------*) ⊢
    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ cat S A B.
@@ -257,15 +265,14 @@ nqed.
 
 unification hint 1 ≔ AA : setoid, B,C : Elang AA;
   AAS ≟ LIST AA,
-  T ≟ ext_powerclass_setoid (list AA),
-  R ≟ mk_unary_morphism1 T (unary_morphism1_setoid1 T T)
-          (λS:Elang AA.
-           mk_unary_morphism1 T T
-            (λS':Elang AA.
-              mk_ext_powerclass (list AA) (cat AA (ext_carr ? S) (ext_carr ? S')) 
-                (ext_prop (list AA) (cat_is_ext AA S S')))
-            (prop11 T T (cat_is_ext_morph AA S)))
-          (prop11 T (unary_morphism1_setoid1 T T) (cat_is_ext_morph AA)),
+  T ≟ ext_powerclass_setoid AAS,
+  R ≟ mk_unary_morphism1 T (unary_morphism1_setoid1 T T) (λX:Elang AA.
+           mk_unary_morphism1 T T (λY:Elang AA.
+             mk_ext_powerclass AAS 
+               (cat AA (ext_carr ? X) (ext_carr ? Y)) 
+               (ext_prop AAS (cat_is_ext AA X Y)))
+             (prop11 T T (fun11 ?? (cat_is_ext_morph AA) X)))
+           (prop11 T (unary_morphism1_setoid1 T T) (cat_is_ext_morph AA)),
    BB ≟ ext_carr ? B,
    CC ≟ ext_carr ? C
 (*------------------------------------------------------*) ⊢
@@ -277,6 +284,50 @@ ndefinition star : ∀A:setoid.∀l:lang A.lang A ≝
   λS.λl.{ w ∈ list S | ∃lw.flatten ? lw = w ∧ conjunct ? lw l}. 
 interpretation "star lang" 'pk l = (star ? l).
 
+(* hints for star *)
+nlemma star_is_morph : ∀A:setoid. (lang A) ⇒_1 (lang A).
+#X; @(λA:lang X.A^* ); #a1 a2 E; @; #x; *; #wl; *; #defx Px; @wl; @; //;
+nelim wl in Px; //; #s tl IH; *; #a1s a1tl; /4/; nqed.
+
+nlemma star_is_ext: ∀A:setoid. (Elang A) → (Elang A).
+ #S A; @ ((ext_carr … A) ^* ); #w1 w2 E; @; *; #wl; *; #defw1 Pwl;
+ @wl; @; //; napply (.=_0 defw1); /2/; nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔ A : setoid, B :  Elang A;
+   AA ≟ LIST A,
+   BB ≟ ext_carr AA B,
+   R ≟ mk_ext_powerclass ? 
+         ((ext_carr ? B)^* ) (ext_prop ? (star_is_ext ? B))
+(*--------------------------------------------------------------------*)  ⊢
+    ext_carr AA R ≡ star A BB.
+    
+unification hint 0 ≔ S:setoid, A:lang (carr S);
+    T ≟ powerclass_setoid (list (carr S)),
+    MM ≟ mk_unary_morphism1 T T 
+               (λB:lang (carr S).star S B) (prop11 T T (star_is_morph S))
+(*--------------------------------------------------------------------------*) ⊢
+   fun11 T T MM A ≡ star S A.
+   
+nlemma star_is_ext_morph:∀A:setoid.(Elang A) ⇒_1 (Elang A).
+#A; @(star_is_ext …);
+#x1 x2 Ex; napply (prop11 … (star_is_morph A)); nassumption.
+nqed.
+
+unification hint 1 ≔ AA : setoid, B : Elang AA;
+  AAS ≟ LIST AA,
+  T ≟ ext_powerclass_setoid AAS,
+  R ≟ mk_unary_morphism1 T T
+            (λS:Elang AA.
+              mk_ext_powerclass AAS (star AA (ext_carr ? S)) 
+                (ext_prop AAS (star_is_ext AA S)))
+            (prop11 T T (star_is_ext_morph AA)),
+   BB ≟ ext_carr ? B
+(*------------------------------------------------------*) ⊢
+   ext_carr AAS (fun11 T T R B) ≡ star AA BB.
+
+(* end hints for star *)
+
 notation > "𝐋 term 70 E" non associative with precedence 75 for @{L_re ? $E}.
 nlet rec L_re (S : Alpha) (r : re S) on r : lang S ≝ 
 match r with
@@ -302,8 +353,8 @@ ndefinition L_re_is_ext : ∀S:Alpha.∀r:re S.Elang S.
 ##| #e H; @; *; #l; *; #defw1 Pl; @l; @; //; napply (.=_1 defw1); /2/; ##]
 nqed.
 
-unification hint 0 ≔ S : Alpha,e : re S; 
-  SS ≟ LIST S,
+unification hint 0 ≔ S : Alpha,e : re (carr (acarr S)); 
+  SS ≟ LIST (acarr S),
   X ≟ mk_ext_powerclass SS (𝐋 e) (ext_prop SS (L_re_is_ext S e))
 (*-----------------------------------------------------------------*)⊢ 
   ext_carr SS X ≡ L_re S e.
@@ -328,14 +379,13 @@ nlemma L_re_is_morph:∀A:Alpha.(setoid1_of_setoid (re A)) ⇒_1 Ω^(list A).
    @; ##[##1,3: nassumption] /2/; ##]
 nqed.
 
-unification hint 0 ≔ A:Alpha, a:re A;
+unification hint 0 ≔ A:Alpha, a:re (carr (acarr A));
   T ≟ setoid1_of_setoid (RE A),
-  T1 ≟ LIST A,
-  T2 ≟ powerclass_setoid T1,
+  T2 ≟ powerclass_setoid (list (carr (acarr A))),
   MM ≟ mk_unary_morphism1 ?? 
-         (λa:setoid1_of_setoid (RE A).𝐋 a) (prop11 ?? (L_re_is_morph A))
+         (λa:carr1 (setoid1_of_setoid (RE A)).𝐋 a) (prop11 ?? (L_re_is_morph A))
 (*--------------------------------------------------------------------------*) ⊢
-   fun11 T T2 MM a ≡  𝐋 a.
+   fun11 T T2 MM a ≡  L_re A a.
    
 nlemma L_re_is_ext_morph:∀A:Alpha.(setoid1_of_setoid (re A)) ⇒_1 𝛀^(list A).
 #A; @; ##[ #a; napply (L_re_is_ext ? a); ##] #a b E;
@@ -345,12 +395,13 @@ ncut (𝐋 b =  𝐋 a); ##[ napply (.=_1 (┼_1 E^-1)); // ] #EL;
 ##| napply (. (# ╪_1 ?)); ##[##3: napply H |##2: ##skip ] napply (EL^-1)]
 nqed.
             
-unification hint 1 ≔  AA : Alpha, a: re AA;
-  T ≟ RE AA, T1 ≟ LIST AA, TT ≟ ext_powerclass_setoid T1,
-  R ≟ mk_unary_morphism1 ??
-       (λa:setoid1_of_setoid T.
-         mk_ext_powerclass ? (𝐋 a) (ext_prop ? (L_re_is_ext AA a)))
-            (prop11 ?? (L_re_is_ext_morph AA))
+unification hint 1 ≔  AA : Alpha, a: re (carr (acarr AA));
+  T ≟ RE AA, T1 ≟ LIST (acarr AA), T2 ≟ setoid1_of_setoid T, 
+  TT ≟ ext_powerclass_setoid T1,
+  R ≟ mk_unary_morphism1 T2 TT
+       (λa:carr1 (setoid1_of_setoid T).
+         mk_ext_powerclass T1 (𝐋 a) (ext_prop T1 (L_re_is_ext AA a)))
+            (prop11 T2 TT (L_re_is_ext_morph AA))
 (*------------------------------------------------------*) ⊢
    ext_carr T1 (fun11 (setoid1_of_setoid T) TT R a) ≡ L_re AA a.
 
@@ -413,13 +464,13 @@ unification hint 0 ≔ SS:Alpha;
     P1 ≟ refl ? (eq0 (PITEM SS)),
     P2 ≟ sym ? (eq0 (PITEM SS)),
     P3 ≟ trans ? (eq0 (PITEM SS)),
-    R ≟ mk_setoid (pitem S) 
+    R ≟ mk_setoid (pitem (carr S)) 
          (mk_equivalence_relation (pitem A) (eq_pitem SS) P1 P2 P3)
 (*-----------------------------------------------------------------*)⊢
     carr R ≡ pitem A.
     
-unification hint 0 ≔ S:Alpha,a,b:pitem S;
-   R ≟ PITEM S,  L ≟ (pitem S)
+unification hint 0 ≔ S:Alpha,a,b:pitem (carr (acarr S));
+   R ≟ PITEM S,  L ≟ pitem (carr (acarr S))
 (* -------------------------------------------- *) ⊢
    eq_pitem S a b ≡ eq_rel L (eq0 R) a b.    
     
@@ -480,9 +531,9 @@ ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
 ##]
 nqed.
 
-unification hint 0 ≔ S : Alpha,e : pitem S; 
-  SS ≟ (list S),
-  X ≟ (mk_ext_powerclass SS (𝐋\p e) (ext_prop SS (L_pi_ext S e)))
+unification hint 0 ≔ S : Alpha,e : pitem (carr (acarr S)); 
+  SS ≟ LIST (acarr S),
+  X ≟ mk_ext_powerclass SS (𝐋\p e) (ext_prop SS (L_pi_ext S e))
 (*-----------------------------------------------------------------*)⊢ 
   ext_carr SS X ≡ 𝐋\p e.
 
@@ -645,7 +696,7 @@ nlemma subW : ∀S.∀a,b:Ω^S.∀w.w ∈ (a - b) → w ∈ a.
 nlemma erase_bull : ∀S:Alpha.∀a:pitem S. |\fst (•a)| = |a|.
 #S a; nelim a; // by {};
 ##[ #e1 e2 IH1 IH2;
-    napply (?^-1);
+    napply (?^-1); 
     napply (.=_0 (IH1^-1)╪_0 (IH2^-1));
     nchange in match (•(e1 · ?)) with (?⊙?);
     ncases (•e1); #e3 b; ncases b; ##[ nnormalize; ncases (•e2); /3/ by refl, conj]
@@ -672,7 +723,7 @@ nqed.
 
 (* XXX This seems to be a pattern for equations *)
 alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
-unification hint 0 ≔ S : Alpha, x,y: re S;
+unification hint 0 ≔ S : Alpha, x,y: re (carr (acarr S));
   SS ≟ RE S,
   TT ≟ setoid1_of_setoid SS,
   T ≟ carr1 TT
@@ -714,16 +765,26 @@ nlemma odot_dot_aux : ∀S:Alpha.∀e1,e2: pre S.
     //]
 nqed.
 
-STOP
+
 
 nlemma sub_dot_star : 
-  ∀S.∀X:word S → Prop.∀b. (X - ϵ b) · X^* ∪ {[]} = X^*.
-#S X b; napply extP; #w; @;
-##[ *; ##[##2: nnormalize; #defw; nrewrite < defw; @[]; @; //]
+  ∀S:Alpha.∀X:Elang S.∀b. (X - ϵ b) · (ext_carr … X)^* ∪ {[]} = (ext_carr … X)^*.
+#S X b; napply ext_set; #w; @;
+##[ *; ##[##2: #defw; @[]; @; //]
     *; #w1; *; #w2; *; *; #defw sube; *; #lw; *; #flx cj;
-    @ (w1 :: lw); nrewrite < defw; nrewrite < flx; @; //;
+    @ (w1 :: lw); @; ##[ napply (.=_0 # ╪_0 flx); napply (?^-1); //]
     @; //; napply (subW … sube);
-##| *; #wl; *; #defw Pwl; nrewrite < defw; nelim wl in Pwl; ##[ #_; @2; //]
+##| *; #wl; *; #defw Pwl; (*  STOP manca ext_carr vs epsilon. *)     
+ncases b; ##[ nchange in match (ϵtrue) with {[]}.
+napply (. (defw^-1 ╪_1 #)); nelim wl in Pwl; /2/;
+#s tl IH; *; #Xs Ptl; ncases s in Xs; ##[ #; napply IH; //] #x xs Xxxs;
+@; @(x :: xs); @(flatten ? tl); @; ##[ @; ##[ napply #] @; //; nassumption; ##]
+nelim tl in Ptl; ##[ #; @[]; /2/] #w ws IH; *; #Xw Pws; @(w :: ws); @; ##[ napply #]
+@; //;
+
+
+
+ nrewrite < defw; nelim wl in Pwl; ##[ #_; @2; //]
     #w' wl' IH; *; #Pw' IHp; nlapply (IH IHp); *;
     ##[ *; #w1; *; #w2; *; *; #defwl' H1 H2;
         @; ncases b in H1; #H1; 
diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index a7a5e74b0..e40dad6f6 100644
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -103,10 +103,11 @@ ndefinition comp_unary_morphisms:
 nqed.
 
 unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2;
-   R ≟ mk_unary_morphism ?? (composition ??? f g)
-        (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
+   R ≟ mk_unary_morphism o1 o3 
+        (composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g))
+        (prop1 o1 o3 (comp_unary_morphisms o1 o2 o3 f g))
  (* -------------------------------------------------------------------- *) ⊢
-     fun1 o1 o3 R ≡ (composition o1 o2 o3 f g).
+    fun1 o1 o3 R ≡ composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g).
 
 ndefinition comp_binary_morphisms: 
   ∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)).
diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 889fb0545..90be6bc94 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -120,10 +120,10 @@ ndefinition comp1_unary_morphisms:
 nqed.
 
 unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2;
-   R ≟ (mk_unary_morphism1 ?? (composition1 ??? f g)
+   R ≟ (mk_unary_morphism1 ?? (composition1 ??? (fun11 ?? f) (fun11 ?? g))
         (prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
  (* -------------------------------------------------------------------- *) ⊢
-       fun11 o1 o3 R ≡ (composition1 o1 o2 o3 f g).
+       fun11 o1 o3 R ≡ composition1 ??? (fun11 ?? f) (fun11 ?? g).
                               
 ndefinition comp1_binary_morphisms:
  ∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 0038ad4f6..c8f303a6b 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -119,20 +119,18 @@ nlemma mem_ext_powerclass_setoid_is_morph:
 [ napply (. (ext_prop … Ha^-1)) | napply (. (ext_prop … Ha)) ] /2/.
 nqed.
 
-unification hint 0 ≔  AA, x, S;  
+unification hint 0 ≔  AA : setoid, S : 𝛀^AA, x : carr AA;  
      A ≟ carr AA,
      SS ≟ (ext_carr ? S),
      TT ≟ (mk_unary_morphism1 ?? 
-             (λx:setoid1_of_setoid ?.
+             (λx:carr1 (setoid1_of_setoid ?).
                mk_unary_morphism1 ??
-                 (λS:ext_powerclass_setoid ?. x ∈ S)
-                 (prop11 ?? (mem_ext_powerclass_setoid_is_morph AA x)))
+                 (λS:carr1 (ext_powerclass_setoid ?). x ∈ (ext_carr ? S))
+                 (prop11 ?? (fun11 ?? (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 AA)
-       (unary_morphism1_setoid1 XX CPROP) TT x S 
-    ≡ mem A SS x.
+     T2 ≟ (ext_powerclass_setoid AA)
+(*---------------------------------------------------------------------------*) ⊢ 
+    fun11 T2 CPROP (fun11 (setoid1_of_setoid AA) (unary_morphism1_setoid1 T2 CPROP) TT x) S ≡ mem A SS x.
 
 nlemma set_ext : ∀S.∀A,B:Ω^S.A =_1 B → ∀x:S.(x ∈ A) =_1 (x ∈ B).
 #S A B; *; #H1 H2 x; @; ##[ napply H1 | napply H2] nqed.
@@ -153,11 +151,15 @@ nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
 nqed.
 
 alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔ 
-  A : setoid, B,C : ext_powerclass A;
-  R ≟ (mk_ext_powerclass ? (B ∩ C) (ext_prop ? (intersect_is_ext ? B C))) 
+unification hint 0 ≔ A : setoid, B,C : 𝛀^A;
+  AA ≟ carr A,
+  BB ≟ ext_carr ? B,
+  CC ≟ ext_carr ? C,
+  R ≟ (mk_ext_powerclass ? 
+        (ext_carr ? B ∩ ext_carr ? C) 
+        (ext_prop ? (intersect_is_ext ? B C))) 
   (* ------------------------------------------*)  ⊢ 
-    ext_carr A R ≡ intersect ? (ext_carr ? B) (ext_carr ? C).
+    ext_carr A R ≡ intersect AA BB CC.
     
 nlemma intersect_is_morph: ∀A. Ω^A ⇒_1 Ω^A ⇒_1 Ω^A.
 #A; napply (mk_binary_morphism1 … (λS,S'. S ∩ S'));
@@ -168,7 +170,8 @@ 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))) 
+       (λX. mk_unary_morphism1 ?? 
+         (λY.X ∩ Y) (prop11 ?? (fun11 ?? (intersect_is_morph A) X))) 
        (prop11 ?? (intersect_is_morph A))
 (*------------------------------------------------------------------------*) ⊢ 
     fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C  ≡ intersect A B C.
@@ -186,12 +189,12 @@ 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 ??
-                (λS':𝛀^AA.
-                  mk_ext_powerclass AA (S∩S') (ext_prop AA (intersect_is_ext ? S S')))
-                (prop11 ?? (intersect_is_ext_morph AA S))) 
+      R ≟ (mk_unary_morphism1 ?? (λX:𝛀^AA.
+               mk_unary_morphism1 ?? (λY:𝛀^AA.
+                  mk_ext_powerclass AA 
+                    (ext_carr ? X ∩ ext_carr ? Y) 
+                    (ext_prop AA (intersect_is_ext ? X Y)))
+                (prop11 ?? (fun11 ?? (intersect_is_ext_morph AA) X))) 
               (prop11 ?? (intersect_is_ext_morph AA))) ,
        BB ≟ (ext_carr ? B),
        CC ≟ (ext_carr ? C)
@@ -217,16 +220,20 @@ nassumption;
 nqed.
 
 alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔
-   A : setoid, B,C :  𝛀^A;
-   R ≟ (mk_ext_powerclass ? (B ∪ C) (ext_prop ? (union_is_ext ? B C)))
+unification hint 0 ≔ A : setoid, B,C :  𝛀^A;
+   AA ≟ carr A,
+   BB ≟ ext_carr ? B,
+   CC ≟ ext_carr ? C,
+   R ≟ mk_ext_powerclass ? 
+         (ext_carr ? B ∪ ext_carr ? C) (ext_prop ? (union_is_ext ? B C))
 (*-------------------------------------------------------------------------*)  ⊢
-    ext_carr A R ≡ union ? (ext_carr ? B) (ext_carr ? C).
+    ext_carr A R ≡ union AA BB CC.
 
 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)))
+        (λA.mk_unary_morphism1 ?? 
+          (λB.A ∪ B) (prop11 ?? (fun11 ?? (union_is_morph S) A)))
         (prop11 ?? (union_is_morph S))
 (*--------------------------------------------------------------------------*) ⊢
    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A ∪ B.
@@ -240,13 +247,12 @@ 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 ??
-            (λS':𝛀^AA.
-              mk_ext_powerclass AA (S ∪ S') (ext_prop AA (union_is_ext ? S S')))
-            (prop11 ?? (union_is_ext_morph AA S)))
-          (prop11 ?? (union_is_ext_morph AA))) ,
+  R ≟ mk_unary_morphism1 ?? (λX:𝛀^AA.
+           mk_unary_morphism1 ?? (λY:𝛀^AA.
+              mk_ext_powerclass AA 
+               (ext_carr ? X ∪ ext_carr ? Y) (ext_prop AA (union_is_ext ? X Y)))
+            (prop11 ?? (fun11 ?? (union_is_ext_morph AA) X)))
+          (prop11 ?? (union_is_ext_morph AA)),
    BB ≟ (ext_carr ? B),
    CC ≟ (ext_carr ? C)
 (*------------------------------------------------------*) ⊢
@@ -268,16 +274,21 @@ nlemma substract_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
 nqed.
 
 alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔
-   A : setoid, B,C :  𝛀^A;
-   R ≟ (mk_ext_powerclass ? (B - C) (ext_prop ? (substract_is_ext ? B C)))
-(*-------------------------------------------------------------------------*)  ⊢
-    ext_carr A R ≡ substract ? (ext_carr ? B) (ext_carr ? C).
+unification hint 0 ≔ A : setoid, B,C :  𝛀^A;
+   AA ≟ carr A,
+   BB ≟ ext_carr ? B,
+   CC ≟ ext_carr ? C,
+   R ≟ mk_ext_powerclass ? 
+         (ext_carr ? B - ext_carr ? C) 
+         (ext_prop ? (substract_is_ext ? B C))
+(*---------------------------------------------------*)  ⊢
+    ext_carr A R ≡ substract AA BB CC.
 
 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)))
+        (λA.mk_unary_morphism1 ?? 
+          (λB.A - B) (prop11 ?? (fun11 ?? (substract_is_morph S) A)))
         (prop11 ?? (substract_is_morph S))
 (*--------------------------------------------------------------------------*) ⊢
    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A - B.
@@ -291,13 +302,13 @@ 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 ??
-            (λS':𝛀^AA.
-              mk_ext_powerclass AA (S - S') (ext_prop AA (substract_is_ext ? S S')))
-            (prop11 ?? (substract_is_ext_morph AA S)))
-          (prop11 ?? (substract_is_ext_morph AA))) ,
+  R ≟ mk_unary_morphism1 ?? (λX:𝛀^AA.
+           mk_unary_morphism1 ?? (λY:𝛀^AA.
+              mk_ext_powerclass AA 
+                (ext_carr ? X - ext_carr ? Y) 
+                (ext_prop AA (substract_is_ext ? X Y)))
+            (prop11 ?? (fun11 ?? (substract_is_ext_morph AA) X)))
+          (prop11 ?? (substract_is_ext_morph AA)),
    BB ≟ (ext_carr ? B),
    CC ≟ (ext_carr ? C)
 (*------------------------------------------------------*) ⊢
@@ -312,37 +323,32 @@ nlemma single_is_ext: ∀A:setoid. A → 𝛀^A.
 #X a; @; ##[ napply ({(a)}); ##] #x y E; @; #H; /3/; nqed. 
 
 alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔ A : setoid, a:A;
+unification hint 0 ≔ A : setoid, a : carr A;
    R ≟ (mk_ext_powerclass ? {(a)} (ext_prop ? (single_is_ext ? a)))
 (*-------------------------------------------------------------------------*)  ⊢
     ext_carr A R ≡ singleton A a.
 
-unification hint 0 ≔ A:setoid, a:A;
+unification hint 0 ≔ A:setoid, a : carr A;
   T ≟ setoid1_of_setoid A,
   AA ≟ carr A,
   MM ≟ mk_unary_morphism1 ?? 
-         (λa:setoid1_of_setoid A.{(a)}) (prop11 ?? (single_is_morph A))
+         (λa:carr1 (setoid1_of_setoid A).{(a)}) (prop11 ?? (single_is_morph 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;
+unification hint 1 ≔ AA : setoid, a: carr AA;
   T ≟ ext_powerclass_setoid AA,
   R ≟ mk_unary_morphism1 ??
-       (λa:setoid1_of_setoid AA.
+       (λa:carr1 (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 (fun11 (setoid1_of_setoid AA) T R a) ≡ singleton AA a.
 
 
-
-
-
-
 (*
 alias symbol "hint_decl" = "hint_decl_Type2".
 unification hint 0 ≔