X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fre%2Fre-setoids.ma;h=ab2d13458928808becfd8616589c91bd2a5bce26;hb=b15a4df27469ee4b64d1b3b8fc996cd15e8a61f0;hp=561ff9d6a62b762f4e7119a5c7686b369bb3bd78;hpb=0ce50c5cdfd8433a29f05774a4977cd050ad474d;p=helm.git

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 561ff9d6a..ab2d13458 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -14,31 +14,32 @@
 
 include "datatypes/pairs.ma".
 include "datatypes/bool.ma".
-include "logic/cprop.ma".
+include "sets/sets.ma".
 
 ninductive Admit : CProp[0] ≝ .
 naxiom admit : Admit.
 
-ninductive list (A:setoid) : Type[0] ≝ 
+ninductive list (A:Type[0]) : Type[0] ≝ 
   | nil: list A
   | cons: A -> list A -> list A.
   
-nlet rec eq_list A (l1, l2 : list A) on l1 : CProp[0] ≝ 
+nlet rec eq_list (A : setoid) (l1, l2 : list A) on l1 : CProp[0] ≝ 
 match l1 with
-[ nil ⇒ match l2 with [ nil ⇒ ? | _ ⇒ ? ]
-| cons x xs ⇒ match l2 with [ nil ⇒ ? | cons y ys ⇒ x = y ∧ eq_list ? xs ys]].
-##[ napply True|napply False|napply False]nqed.
+[ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ True | _ ⇒ False ]
+| cons x xs ⇒ match l2 with [ nil ⇒ False | cons y ys ⇒ x = y ∧ eq_list ? xs ys]].
    
 ndefinition LIST : setoid → setoid.
 #S; @(list S); @(eq_list S); ncases admit; nqed.  
 
-unification hint 0 ≔ S;
-  P1 ≟ refl ? (eq (LIST S)),
-  P2 ≟ sym ? (eq (LIST S)),
-  P3 ≟ trans ? (eq (LIST S)),
-  X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list S) P1 P2 P3)
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+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 S) P1 P2 P3),
+  T ≟ carr S
 (*-----------------------------------------------------------------------*) ⊢
-     carr X ≡ list S.
+     carr X ≡ list T.
 
 notation "hvbox(hd break :: tl)"
   right associative with precedence 47
@@ -62,7 +63,7 @@ nlet rec append A (l1: list A) l2 on l1 ≝
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-ntheorem append_nil: ∀A.∀l:list A.l @ [] = l.
+ntheorem append_nil: ∀A:setoid.∀l:list A.l @ [] = l.
 #A;#l;nelim l;//; #a;#l1;#IH;nnormalize;/2/;nqed.
 
 ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) = f (f x y) z. 
@@ -70,13 +71,16 @@ ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) =
 ninductive one : Type[0] ≝ unit : one.
 
 ndefinition force ≝ 
-  λS:Type[1].λs:S.λT:Type[1].λt:T.λlock:one.
-    match lock return λ_.Type[1] with [ unit ⇒ T].
+  λS:Type[2].λs:S.λT:Type[2].λt:T.λlock:one.
+    match lock return λ_.Type[2] with [ unit ⇒ T].
 
-nlet rec lift (S:Type[1]) (s:S) (T:Type[1]) (t:T) (lock:one) on lock : force S s T t lock ≝ 
+nlet rec lift (S:Type[2]) (s:S) (T:Type[2]) (t:T) (lock:one) on lock : force S s T t lock ≝ 
  match lock return λlock.force S s T t lock with [ unit ⇒ t ].
 
-ncoercion lift : ∀S:Type[1].∀s:S.∀T:Type[1].∀t:T.∀lock:one. force S s T t lock ≝ lift
+ncoercion lift1 : ∀S:Type[1].∀s:S.∀T:Type[1].∀t:T.∀lock:one. force S s T t lock ≝ lift
+ on s : ? to force ?????.
+
+ncoercion lift2 : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock ≝ lift
  on s : ? to force ?????.
 
 unification hint 0 ≔ R : setoid; 
@@ -84,23 +88,64 @@ unification hint 0 ≔ R : setoid;
 (* ---------------------------------------- *) ⊢ 
    setoid ≡ force ?(*Type[0]*) MR TR R lock.
 
-ntheorem associative_append: ∀A.associative (list A) (append A).
+unification hint 0 ≔ R : setoid1; 
+   TR ≟ setoid1, MR ≟ (carr1 R), lock ≟ unit 
+(* ---------------------------------------- *) ⊢ 
+   setoid1 ≡ force ? MR TR R lock.
+
+ntheorem associative_append: ∀A:setoid.associative (list A) (append A).
 #A;#x;#y;#z;nelim x[//|#a;#x1;#H;nnormalize;/2/]nqed.
 
 interpretation "iff" 'iff a b = (iff a b).  
 
+ninductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝ refl: eq A x x.
+
+nlemma eq_rect_Type0_r':
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
+ #A; #a; #x; #p; ncases p; #P; #H; nassumption.
+nqed.
+
+nlemma eq_rect_Type0_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
+nqed.
+
+nlemma eq_rect_CProp0_r':
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
+ #A; #a; #x; #p; ncases p; #P; #H; nassumption.
+nqed.
+
+nlemma eq_rect_CProp0_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
+nqed.
+
+notation < "a = b" non associative with precedence 45 for @{ 'eqpp $a $b}.
+interpretation "bool eq" 'eqpp a b = (eq bool a b). 
+
+ndefinition BOOL : setoid.
+@bool; @(eq bool); ncases admit.nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+alias id "refl" = "cic:/matita/ng/properties/relations/refl.fix(0,1,3)".
+unification hint 0 ≔ ;
+  P1 ≟ refl ? (eq0 BOOL),
+  P2 ≟ sym ? (eq0 BOOL),
+  P3 ≟ trans ? (eq0 BOOL),
+  X ≟ mk_setoid bool (mk_equivalence_relation ? (eq bool) P1 P2 P3)
+(*-----------------------------------------------------------------------*) ⊢
+     carr X ≡ bool.
+
 nrecord Alpha : Type[1] ≝ { 
-   carr :> setoid;
-   eqb: carr → carr → bool; (*
-   eqb_true: ∀x,y. (eqb x y = true) = (x = y) *)
+   acarr :> setoid;
+   eqb: acarr → acarr → bool; 
+   eqb_true: ∀x,y. (eqb x y = true) = (x = y)
 }.
  
 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 interpretation "eqb" 'eqb a b = (eqb ? a b).
 
-ndefinition word ≝ λS:Alpha.list S.
-
-ninductive re (S: Alpha) : Type[0] ≝
+ninductive re (S: Type[0]) : Type[0] ≝
    z: re S
  | e: re S
  | s: S → re S
@@ -108,8 +153,23 @@ ninductive re (S: Alpha) : Type[0] ≝
  | o: re S → re S → re S
  | k: re S → re S.
  
+naxiom eq_re : ∀S:Alpha.re S → re S → CProp[0].
+ndefinition RE : Alpha → setoid.
+#A; @(re A); @(eq_re A); ncases admit. nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+alias id "carr" = "cic:/matita/ng/sets/setoids/carr.fix(0,0,1)".
+unification hint 0 ≔ A : Alpha;
+  P1 ≟ refl ? (eq0 (RE A)),
+  P2 ≟ sym ? (eq0 (RE A)),
+  P3 ≟ trans ? (eq0 (RE A)),
+  X ≟ mk_setoid (re A) (mk_equivalence_relation ? (eq_re A) P1 P2 P3),
+  T ≟ acarr A
+(*-----------------------------------------------------------------------*) ⊢
+     carr X ≡ (re T).
+
 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
-notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
+notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
 interpretation "star" 'pk a = (k ? a).
 interpretation "or" 'plus a b = (o ? a b).
            
@@ -117,7 +177,7 @@ notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
 interpretation "cat" 'pc a b = (c ? a b).
 
 (* to get rid of \middot *)
-ncoercion c  : ∀S:Alpha.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?.
+ncoercion c  : ∀S.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?.
 
 notation < "a" non associative with precedence 90 for @{ 'ps $a}.
 notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
@@ -126,55 +186,59 @@ interpretation "atom" 'ps a = (s ? a).
 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
 interpretation "epsilon" 'epsilon = (e ?).
 
-notation "∅" non associative with precedence 90 for @{ 'empty }.
+notation "0" non associative with precedence 90 for @{ 'empty }.
 interpretation "empty" 'empty = (z ?).
 
-nlet rec flatten (S : Alpha) (l : list (word S)) on l : word S ≝ 
+notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }.
+notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }.
+
+nlet rec flatten S (l : list (list S)) on l : list S ≝ 
 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
 
-nlet rec conjunct (S : Alpha) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
-match l with [ nil ⇒ ? | cons w tl ⇒ r w ∧ conjunct ? tl r ]. napply True. nqed.
+nlet rec conjunct S (l : list (list S)) (L : lang S) on l: CProp[0] ≝
+match l with [ nil ⇒ True | cons w tl ⇒ w ∈ L ∧ conjunct ? tl L ].
+
 
-ndefinition empty_lang ≝ λS.λw:word S.False.
+ndefinition empty_set : ∀A.Ω^A ≝ λA.{ w | False }.
+notation "∅" non associative with precedence 90 for @{'emptyset}.
+interpretation "empty set" 'emptyset = (empty_set ?).
+
+(*
 notation "{}" non associative with precedence 90 for @{'empty_lang}.
 interpretation "empty lang" 'empty_lang = (empty_lang ?).
+*)
 
-ndefinition sing_lang ≝ λS.λx,w:word S.x=w.
-notation "{x}" non associative with precedence 90 for @{'sing_lang $x}.
-interpretation "sing lang" 'sing_lang x = (sing_lang ? x).
+ndefinition sing_lang : ∀A:setoid.∀x:A.Ω^A ≝ λS.λx.{ w | x = w }.
+interpretation "sing lang" 'singl x = (sing_lang ? x).
 
-ndefinition union : ∀S,l1,l2,w.Prop ≝ λS.λl1,l2.λw:word S.l1 w ∨ l2 w.
-interpretation "union lang" 'union a b = (union ? a b).
+interpretation "subset construction with type" 'comprehension t \eta.x = 
+  (mk_powerclass t x).
 
-ndefinition cat : ∀S,l1,l2,w.Prop ≝ 
-  λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
+ndefinition cat : ∀A:setoid.∀l1,l2:lang A.lang A ≝ 
+  λS.λl1,l2.{ w ∈ list S | ∃w1,w2.w =_0 w1 @ w2 ∧ w1 ∈ l1 ∧ w2 ∈ l2}.
 interpretation "cat lang" 'pc a b = (cat ? a b).
 
-ndefinition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. 
+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).
 
-notation > "𝐋 term 90 E" non associative with precedence 90 for @{in_l ? $E}.
-nlet rec in_l (S : Alpha) (r : re S) on r : word S → Prop ≝ 
+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
-[ z ⇒ {}
+[ z ⇒ ∅
 | e ⇒ { [ ] }
 | s x ⇒ { [x] }
 | c r1 r2 ⇒ 𝐋 r1 · 𝐋 r2
 | o r1 r2 ⇒  𝐋 r1 ∪ 𝐋 r2
 | k r1 ⇒ (𝐋 r1) ^*].
-notation "𝐋 term 90 E" non associative with precedence 90 for @{'in_l $E}.
-interpretation "in_l" 'in_l E = (in_l ? E).
-interpretation "in_l mem" 'mem w l = (in_l ? l w).
+notation "𝐋 term 70 E" non associative with precedence 75 for @{'L_re $E}.
+interpretation "in_l" 'L_re E = (L_re ? E).
 
 notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
+ndefinition orb ≝ λa,b:bool. match a with [ true ⇒ true | _ ⇒ b ].
 interpretation "orb" 'orb a b = (orb a b).
 
-ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
-notation > "'if' term 19 e 'then' term 19 t 'else' term 19 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
-interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
-
-ninductive pitem (S: Alpha) : Type[0] ≝
+ninductive pitem (S: Type[0]) : Type[0] ≝
    pz: pitem S
  | pe: pitem S
  | ps: S → pitem S
@@ -185,6 +249,11 @@ ninductive pitem (S: Alpha) : Type[0] ≝
  
 ndefinition pre ≝ λS.pitem S × bool.
 
+notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
+interpretation "fst" 'fst x = (fst ? ? x).
+notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
+interpretation "snd" 'snd x = (snd ? ? x).
+
 interpretation "pstar" 'pk a = (pk ? a).
 interpretation "por" 'plus a b = (po ? a b).
 interpretation "pcat" 'pc a b = (pc ? a b).
@@ -200,68 +269,172 @@ interpretation "pempty" 'empty = (pz ?).
 notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}.
 nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
  match l with
-  [ pz ⇒ ∅
+  [ pz ⇒ 0
   | pe ⇒ ϵ
   | ps x ⇒ `x
   | pp x ⇒ `x
   | pc E1 E2 ⇒ (|E1| · |E2|)
   | po E1 E2 ⇒ (|E1| + |E2|)
   | pk E ⇒ |E|^* ].
-notation < ".|term 19 e|" non associative with precedence 70 for @{'forget $e}.
+notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.
 interpretation "forget" 'forget a = (forget ? a).
 
-notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
-interpretation "fst" 'fst x = (fst ? ? x).
-notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
-interpretation "snd" 'snd x = (snd ? ? x).
-
-notation > "𝐋\p\ term 90 E" non associative with precedence 90 for @{in_pl ? $E}.
-nlet rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝ 
+notation > "𝐋\p\ term 70 E" non associative with precedence 75 for @{L_pi ? $E}.
+nlet rec L_pi (S : Alpha) (r : pitem S) on r : lang S ≝ 
 match r with
-[ pz ⇒ {}
-| pe ⇒ {}
-| ps _ ⇒ {}
+[ pz ⇒ ∅
+| pe ⇒ ∅
+| ps _ ⇒ ∅
 | pp x ⇒ { [x] }
-| pc r1 r2 ⇒ 𝐋\p\ r1 · 𝐋 .|r2| ∪ 𝐋\p\ r2
+| pc r1 r2 ⇒ 𝐋\p\ r1 · 𝐋 |r2| ∪ 𝐋\p\ r2
 | po r1 r2 ⇒ 𝐋\p\ r1 ∪ 𝐋\p\ r2
-| pk r1 ⇒ 𝐋\p\ r1 · 𝐋 (.|r1|^* ) ].
-notation > "𝐋\p term 90 E" non associative with precedence 90 for @{'in_pl $E}.
-notation "𝐋\sub(\p) term 90 E" non associative with precedence 90 for @{'in_pl $E}.
-interpretation "in_pl" 'in_pl E = (in_pl ? E).
-interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
+| pk r1 ⇒ 𝐋\p\ r1 · 𝐋 (|r1|^* ) ].
+notation > "𝐋\p term 70 E" non associative with precedence 75 for @{'L_pi $E}.
+notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi $E}.
+interpretation "in_pl" 'L_pi E = (L_pi ? E).
+
+unification hint 0 ≔ S,a,b;
+   R ≟ LIST S,
+   L ≟ (list S)
+(* -------------------------------------------- *) ⊢
+   eq_list S a b ≡ eq_rel L (eq0 R) a b.
+   
+ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.   
+   
+alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
+unification hint 0 ≔ S : setoid, x,y;
+  SS ≟ LIST S,
+  TT ≟ setoid1_of_setoid SS
+(*-----------------------------------------*) ⊢ 
+  eq_list S x y ≡ eq_rel1 ? (eq1 TT) x y.
+  
+unification hint 0 ≔ SS : setoid;
+  S ≟ carr SS,
+  TT ≟ setoid1_of_setoid (LIST SS)
+(*-----------------------------------------------------------------*) ⊢ 
+  list S ≡ carr1 TT.
+
+notation > "B ⇒_0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
+notation > "B ⇒_1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
+notation "B ⇒\sub 0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
+notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
 
-ndefinition epsilon ≝ λS,b.if b then { ([ ] : word S) } else {}.
+interpretation "unary morphism 0" 'umorph0 A B = (unary_morphism A B).
+interpretation "unary morphism 1" 'umorph1 A B = (unary_morphism1 A B).
+
+
+nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP).
+  ∀y,z:T.y = z → (∀x.y=z → P x y = P x z)  → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)).
+#S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed.
+
+notation "∑" non associative with precedence 90 for @{Sig ?????}.
+
+nlemma test : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y → (Ex S (λw.ee x w ∧ True)) =_1 (Ex S (λw.ee y w ∧ True)).
+#S m x y E;
+napply (.=_1 (∑ E (λw,H.(H ╪_1 #)╪_1 #))).
+napply #.
+nqed.
+
+nlemma test2 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y → 
+   (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
+#S m x y E;
+napply (.=_1 #╪_1(∑ E (λw,H.(H ╪_1 #) ╪_1 #))).
+napply #.
+nqed.
+
+nlemma ex_setoid : ∀S:setoid.(S ⇒_1 CPROP) → setoid.
+#T P; @ (Ex T (λx:T.P x)); @;
+##[ #H1 H2; napply True |##*: //; ##]
+nqed.
+
+unification hint 0 ≔ T,P ; S ≟ (ex_setoid T P) ⊢
+ Ex T (λx:T.P x) ≡ carr S.
+
+nlemma test3 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y → 
+   ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
+#S m x y E;
+napply (.=_1 (∑ E (λw,H.(H ╪_1 #) ╪_1 #)) ╪_1 #).
+napply #.
+nqed.
+
+ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
+#S r; @(𝐋\p r); #w1 w2 E; nelim r; 
+##[ /2/;
+##| /2/;
+##| #x; @; *;
+##| #x; @; #H; nchange in H with ([?] =_0 ?); ##[ napply ((.=_0 H) E); ##]
+    napply ((.=_0 H) E^-1);
+##| #e1 e2 H1 H2; 
+    nchange in match (w1 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
+    nchange in match (w2 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
+    napply (.= (#‡H2));
+    napply (.=_1 (∑ E (λx1,H1.∑ E (λx2,H2.?)))╪_1 #); ##[
+      ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
+        @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
+      napply ( (X‡#)‡#); ##]
+    napply #;
+##| #e1 e2 H1 H2;
+    nnormalize in ⊢ (???%%);
+    napply (H1‡H2);
+##| #e H; nnormalize in ⊢ (???%%);
+    napply (.=_1 (∑ E (λx1,H1.∑ E (λx2,H2.?)))); ##[
+      ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
+        @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
+      napply ((X‡#)‡#); ##]
+    napply #;##] 
+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)))
+(*-----------------------------------------------------------------*)⊢ 
+  ext_carr SS X ≡ 𝐋\p e.
+  
+ndefinition epsilon ≝ 
+  λS:Alpha.λb.match b return λ_.lang S with [ true ⇒ { [ ] } | _ ⇒ ∅ ].
 
 interpretation "epsilon" 'epsilon = (epsilon ?).
 notation < "ϵ b" non associative with precedence 90 for @{'app_epsilon $b}.
 interpretation "epsilon lang" 'app_epsilon b = (epsilon ? b).
 
-ndefinition in_prl ≝ λS : Alpha.λp:pre S.  𝐋\p\ (\fst p) ∪ ϵ (\snd p).
+ndefinition L_pr ≝ λS : Alpha.λp:pre S.  𝐋\p\ (\fst p) ∪ ϵ (\snd p).
   
-interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
-interpretation "in_prl" 'in_pl E = (in_prl ? E).
-
-nlemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ].
-#S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct; nqed.
+interpretation "L_pr" 'L_pi E = (L_pr ? E).
 
+nlemma append_eq_nil : ∀S:setoid.∀w1,w2:list S. [ ] = w1 @ w2 → w1 = [ ].
+#S w1; ncases w1; //. nqed.
+  
 (* lemma 12 *)
-nlemma epsilon_in_true : ∀S.∀e:pre S. [ ] ∈ e ↔ \snd e = true.
+nlemma epsilon_in_true : ∀S:Alpha.∀e:pre S. [ ] ∈ 𝐋\p e = (\snd e = true).
 #S r; ncases r; #e b; @; ##[##2: #H; nrewrite > H; @2; /2/; ##] ncases b;//; 
-nnormalize; *; ##[##2:*] nelim e;
-##[ ##1,2: *; ##| #c; *; ##| #c; nnormalize; #; ndestruct; ##| ##7: #p H;
-##| #r1 r2 H G; *; ##[##2: /3/ by or_intror]
-##| #r1 r2 H1 H2; *; /3/ by or_intror, or_introl; ##]
-*; #w1; *; #w2; *; *; #defw1; nrewrite > (append_eq_nil … w1 w2 …); /3/ by {};//;
+*; ##[##2:*] nelim e;
+##[ ##1,2: *; ##| #c; *; ##| #c; *| ##7: #p H;
+##| #r1 r2 H G; *; ##[##2: nassumption; ##]
+##| #r1 r2 H1 H2; *; /2/ by {}]
+*; #w1; *; #w2; *; *; 
+##[ #defw1 H1 foo; napply H;
+    napply (. (append_eq_nil ? ?? defw1)^-1╪_1#);
+    nassumption; 
+##| #defw1 H1 foo; napply H;
+    napply (. (append_eq_nil ? ?? defw1)^-1╪_1#);
+    nassumption; 
+##]
 nqed.
 
-nlemma not_epsilon_lp : ∀S.∀e:pitem S. ¬ (𝐋\p e [ ]).
-#S e; nelim e; nnormalize; /2/ by nmk;
-##[ #; @; #; ndestruct;
-##| #r1 r2 n1 n2; @; *; /2/; *; #w1; *; #w2; *; *; #H;
-    nrewrite > (append_eq_nil …H…); /2/;
-##| #r1 r2 n1 n2; @; *; /2/;
-##| #r n; @; *; #w1; *; #w2; *; *; #H;     
-    nrewrite > (append_eq_nil …H…); /2/;##]
+nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ([ ] ∈ (𝐋\p e)).
+#S e; nelim e; ##[##1,2,3,4: nnormalize;/2/]
+##[ #p1 p2 np1 np2; *; ##[##2: napply np2] *; #w1; *; #w2; *; *; #abs;
+    nlapply (append_eq_nil ??? abs); # defw1; #; napply np1;
+    napply (. defw1^-1╪_1#);
+    nassumption;
+##| #p1 p2 np1 np2; *; nchange with (¬?); //;
+##| #r n; *; #w1; *; #w2; *; *; #abs; #; napply n;
+    nlapply (append_eq_nil ??? abs); # defw1; #;
+    napply (. defw1^-1╪_1#);
+    nassumption;##]
 nqed.
 
 ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
@@ -286,12 +459,12 @@ ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
 
 notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.
 interpretation "lk" 'lk op a = (lk ? op a).
-notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
+notation > "a ^ ⊛" non associative with precedence 75 for @{'lk eclose $a}.
 
 notation > "•" non associative with precedence 60 for @{eclose ?}.
 nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
  match E with
-  [ pz ⇒ 〈 ∅, false 〉
+  [ pz ⇒ 〈 0, false 〉
   | pe ⇒ 〈 ϵ,  true 〉
   | ps x ⇒ 〈 `.x, false 〉
   | pp x ⇒ 〈 `.x, false 〉
@@ -305,48 +478,123 @@ notation > "• x" non associative with precedence 60 for @{'eclose $x}.
 ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
 interpretation "reclose" 'eclose x = (reclose ? x).
 
-ndefinition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w.
-notation > "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
-notation "A =\sub 1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
-interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b).
+nlemma cup0 :∀S.∀p:lang S.p ∪ ∅ = p.
+#S p; @; #w; ##[*; //| #; @1; //] *; nqed.
 
-naxiom extP : ∀S.∀p,q:word S → Prop.(p =1 q) → p = q.
+nlemma cupC : ∀S. ∀a,b:lang S.a ∪ b = b ∪ a.
+#S a b; @; #w; *; nnormalize; /2/; nqed.
+
+nlemma cupID : ∀S. ∀a:lang S.a ∪ a = a.
+#S a; @; #w; ##[*; //] /2/; nqed.
 
 nlemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) = ϵ b1 ∪ ϵ b2. ##[##2: napply S]
-#S b1 b2; ncases b1; ncases b2; napply extP; #w; nnormalize; @; /2/; *; //; *;
+#S b1 b2; ncases b1; ncases b2; 
+nchange in match (true || true) with true;
+nchange in match (true || false) with true;
+nchange in match (ϵ true) with {[]};
+nchange in match (ϵ false) with ∅;
+##[##1,4: napply ((cupID…)^-1);
+##| napply ((cup0 S {[]})^-1);
+##| napply (.= (cup0 S {[]})^-1); napply cupC; ##]
+nqed.
+
+nlemma cupA : ∀S.∀a,b,c:lang S.a ∪ b ∪ c = a ∪ (b ∪ c).
+#S a b c; @; #w; *; /3/; *; /3/; nqed.
+
+nlemma setP : ∀S.∀A,B:Ω^S.∀x:S. A = B → (x ∈ A) = (x ∈ B).
+#S A B x; *; #H1 H2; @; ##[ napply H1 | napply H2] nqed.
+
+nlemma pset_ext : ∀S.∀A,B:Ω^S.(∀x:S. (x ∈ A) = (x ∈ B)) → A = B.
+#S A B H; @; #x; ncases (H x); #H1 H2; ##[ napply H1 | napply H2] nqed.
+
+ndefinition if': ∀A,B:CPROP. A = B → A → B.
+#A B; *; /2/. nqed.
+
+ncoercion if : ∀A,B:CPROP. ∀p:A = B. A → B ≝ if' on _p : eq_rel1 ???? to ∀_:?.?.
+
+(* move in sets.ma? *)
+nlemma union_morphism : ∀A.Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
+#X; napply (mk_binary_morphism1 … (λA,B.A ∪ B));
+#A1 A2 B1 B2 EA EB; napply pset_ext; #x;
+nchange in match (x ∈ (A1 ∪ B1)) with (?∨?);
+napply (.= (setP ??? x EA)‡#);
+napply (.= #‡(setP ??? x EB)); //;
 nqed.
 
-nlemma cupA : ∀S.∀a,b,c:word S → Prop.a ∪ b ∪ c = a ∪ (b ∪ c).
-#S a b c; napply extP; #w; nnormalize; @; *; /3/; *; /3/; nqed.
+nlemma union_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
+ #S A B; @ (A ∪ B); #x y Exy; @; *; #H1; 
+##[##1,3: @; ##|##*: @2 ]
+##[##1,3: napply (. (Exy^-1)╪_1#) 
+##|##2,4: napply (. Exy╪_1#)]
+nassumption;
+nqed.
 
-nlemma cupC : ∀S. ∀a,b:word S → Prop.a ∪ b = b ∪ a.
-#S a b; napply extP; #w; @; *; nnormalize; /2/; 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)))
+  (* ----------------------------------------------------------------*)  ⊢
+    ext_carr A R ≡ union ? (ext_carr ? B) (ext_carr ? C).
+
+unification hint 0 ≔ S:Type[0], A,B:Ω^S;
+  MM ≟ mk_unary_morphism1 ??
+        (λA.mk_unary_morphism1 ?? (λB.A ∪ B) (prop11 ?? (union_morphism S A)))
+        (prop11 ?? (union_morphism S))
+ (*-----------------------------------------------------*) ⊢
+   fun11 ?? (fun11 ?? MM A) B ≡ A ∪ B.
+   
+nlemma union_is_ext_morph:∀A:setoid.𝛀^A ⇒_1 (𝛀^A ⇒_1 𝛀^A).
+#A; napply (mk_binary_morphism1 …  (union_is_ext …));
+#x1 x2 y1 y2 Ex Ey; napply (prop11 … (union_morphism A)); nassumption.
+nqed.
+            
+unification hint 1 ≔
+      AA : setoid, B,C : 𝛀^AA;
+      A ≟ carr AA,
+      R ≟ (mk_unary_morphism1 ??
+              (λS:(*ext_powerclass_setoid AA*)𝛀^AA.
+               mk_unary_morphism1 ??
+                (λS':(*ext_powerclass_setoid AA*)𝛀^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))) ,
+       BB ≟ (ext_carr ? B),
+       CC ≟ (ext_carr ? C)
+   (* ------------------------------------------------------*) ⊢
+            ext_carr AA (R B C) ≡ union A BB CC.
 
+   
 (* theorem 16: 2 *)
 nlemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.𝐋\p (e1 ⊕ e2) = 𝐋\p e1 ∪ 𝐋\p e2.
 #S r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2;
-nwhd in ⊢ (??(??%)?);
-nchange in ⊢(??%?) with (𝐋\p (e1 + e2) ∪ ϵ (b1 || b2));
-nchange in ⊢(??(??%?)?) with (𝐋\p (e1) ∪ 𝐋\p (e2));
-nrewrite > (epsilon_or S …); nrewrite > (cupA S (𝐋\p e1) …);
-nrewrite > (cupC ? (ϵ b1) …); nrewrite < (cupA S (𝐋\p e2) …);
-nrewrite > (cupC ? ? (ϵ b1) …); nrewrite < (cupA …); //;
+nwhd in ⊢ (???(??%)?);
+nchange in ⊢(???%?) with (𝐋\p (e1 + e2) ∪ ϵ (b1 || b2));
+nchange in ⊢(???(??%?)?) with (𝐋\p (e1) ∪ 𝐋\p (e2));
+napply (.= #╪_1 (epsilon_or ???));
+napply (.= (cupA…)^-1);
+napply (.= (cupA…)╪_1#);
+napply (.= (#╪_1(cupC…))╪_1#);
+napply (.= (cupA…)^-1╪_1#);
+napply (.= (cupA…));
+//;
 nqed.
 
+FINQUI
+
+manca setoide per pair (e pre)
+
 nlemma odotEt : 
-  ∀S.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = 〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
+  ∀S:Alpha.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = ?.〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
 #S e1 e2 b2; nnormalize; ncases (•e2); //; nqed.
 
 nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) =  𝐋\p e1 · 𝐋 .|e2| ∪ 𝐋\p e2. //; nqed.
 
-nlemma cup_dotD : ∀S.∀p,q,r:word S → Prop.(p ∪ q) · r = (p · r) ∪ (q · r). 
+nlemma cup_dotD : ∀S.∀p,q,r:lang S.(p ∪ q) · r = (p · r) ∪ (q · r). 
 #S p q r; napply extP; #w; nnormalize; @; 
 ##[ *; #x; *; #y; *; *; #defw; *; /7/ by or_introl, or_intror, ex_intro, conj;
 ##| *; *; #x; *; #y; *; *; /7/ by or_introl, or_intror, ex_intro, conj; ##]
 nqed.
 
-nlemma cup0 :∀S.∀p:word S → Prop.p ∪ {} = p.
-#S p; napply extP; #w; nnormalize; @; /2/; *; //; *; nqed.
 
 nlemma erase_dot : ∀S.∀e1,e2:pitem S.𝐋 .|e1 · e2| =  𝐋 .|e1| · 𝐋 .|e2|.
 #S e1 e2; napply extP; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj;