From 90ff94e74ceed0954b8599bff55d5c84f15c1b9f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 23 Sep 2010 22:39:08 +0000
Subject: [PATCH] morphism support moved to sets/ and logic/cprop

---
 helm/software/matita/nlibrary/logic/cprop.ma  | 165 ++++++++++-
 .../software/matita/nlibrary/re/re-setoids.ma | 261 +++++-------------
 helm/software/matita/nlibrary/sets/setoids.ma |   9 +-
 .../software/matita/nlibrary/sets/setoids1.ma |  15 +-
 helm/software/matita/nlibrary/sets/sets.ma    | 103 ++++++-
 5 files changed, 350 insertions(+), 203 deletions(-)

diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
index 47ccef5d0..1efc042ff 100644
--- a/helm/software/matita/nlibrary/logic/cprop.ma
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -88,4 +88,167 @@ unification hint 0 ≔ A,B ⊢
  mk_unary_morphism1 …
   (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
   (prop11 … if_morphism)
-  A B ≡ A → B.
\ No newline at end of file
+  A B ≡ A → B.
+  
+(* not as morphism *)
+nlemma Not_morphism : CProp[0] ⇒_1 CProp[0].
+@(λx:CProp[0].¬ x); #a b; *; #; @; /3/; nqed.
+
+unification hint 0 ≔ P : CProp[0];
+   A ≟ CPROP, 
+   B ≟ CPROP,
+   M ≟ mk_unary_morphism1 ?? (λP.¬ P) (prop11 ?? Not_morphism)
+(*------------------------*)⊢
+  fun11 A B M P ≡ ¬ P.
+
+(* Ex setoid support *)
+
+(* The caml, as some patches for it 
+ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
+*)
+
+(* simple case where the whole predicate can be rewritten *)
+nlemma Ex_morphism : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
+#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];
+   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))
+(*------------------------*)⊢
+  fun11 A B M P ≡ Ex 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];
+   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))
+(*------------------------*)⊢
+  fun11 A B M P ≡ Ex 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 ; 
+   S ≟ (Ex_setoid T P) 
+(*---------------------------*) ⊢
+   Ex T (λx:T.P x) ≡ carr S.
+
+(* couts how many Ex we are traversing *)
+ninductive counter : Type[0] ≝ 
+ | End : counter 
+ | Next : (Prop → Prop) → (* dummy arg please the notation mechanism *)
+          counter → counter. 
+
+(* to rewrite terms (live in setoid) *)
+nlet rec mk_P (S, T : setoid) (n : counter) on n ≝ 
+  match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P S T m) ].
+
+nlet rec mk_F (S, T : setoid) (n : counter) on n ≝ 
+  match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F S T m) ].
+  
+nlet rec mk_E (S, T : setoid) (n : counter) on n : ∀f,g : mk_F S T n. CProp[0] ≝ 
+  match n with 
+  [ End ⇒ λf,g:T. f = g 
+  | Next q m ⇒ λf,g: mk_F S T (Next q m). ∀x:S.mk_E S T m (f x) (g x) ].
+
+nlet rec mk_H (S, T : setoid) (n : counter) on n : 
+∀P1,P2: mk_P S T n.∀f,g : mk_F S T n. CProp[1] ≝ 
+  match n with 
+  [ End ⇒ λP1,P2:mk_P S T End.λf,g:T. f = g → P1 f =_1 P2 g 
+  | Next q m ⇒ λP1,P2: mk_P S T (Next q m).λf,g: mk_F S T (Next q m). 
+              ∀x:S.mk_H S T m (P1 x) (P2 x) (f x) (g x) ].
+
+nlet rec mk_Ex (S, T : setoid) (n : counter) on n : 
+∀P: mk_P S T n.∀f : mk_F S T n. CProp[0] ≝ 
+  match n with 
+  [ End ⇒ λP:mk_P S T End.λf:T. P f 
+  | Next q m ⇒ λP: mk_P S T (Next q m).λf: mk_F S T (Next q m). 
+              ∃x:S.mk_Ex S T m (P x) (f x) ].
+
+nlemma Sig_generic : ∀S,T.∀n:counter.∀P,f,g.
+  mk_E S T n f g → mk_H S T n P P f g → mk_Ex S T n P f =_1 mk_Ex S T n P g.
+#S T n; nelim n; nnormalize;
+##[ #P f g E H; /2/;
+##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
+nqed.
+
+(* to rewrite propositions (live in setoid1) *)
+nlet rec mk_P1 (S : setoid) (T : setoid1) (n : counter) on n ≝ 
+  match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P1 S T m) ].
+
+nlet rec mk_F1 (S : setoid) (T : setoid1) (n : counter) on n ≝ 
+  match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F1 S T m) ].
+  
+nlet rec mk_E1 (S : setoid) (T : setoid1) (n : counter) on n : ∀f,g : mk_F1 S T n. CProp[1] ≝ 
+  match n with 
+  [ End ⇒ λf,g:T. f =_1 g 
+  | Next q m ⇒ λf,g: mk_F1 S T (Next q m). ∀x:S.mk_E1 S T m (f x) (g x) ].
+
+nlet rec mk_H1 (S : setoid) (T : setoid1) (n : counter) on n : 
+∀P1,P2: mk_P1 S T n.∀f,g : mk_F1 S T n. CProp[1] ≝ 
+  match n with 
+  [ End ⇒ λP1,P2:mk_P1 S T End.λf,g:T. f = g → P1 f =_1 P2 g 
+  | Next q m ⇒ λP1,P2: mk_P1 S T (Next q m).λf,g: mk_F1 S T (Next q m). 
+              ∀x:S.mk_H1 S T m (P1 x) (P2 x) (f x) (g x) ].
+
+nlet rec mk_Ex1 (S : setoid) (T : setoid1) (n : counter) on n : 
+∀P: mk_P1 S T n.∀f : mk_F1 S T n. CProp[0] ≝ 
+  match n with 
+  [ End ⇒ λP:mk_P1 S T End.λf:T. P f 
+  | Next q m ⇒ λP: mk_P1 S T (Next q m).λf: mk_F1 S T (Next q m). 
+              ∃x:S.mk_Ex1 S T m (P x) (f x) ].
+
+nlemma Sig_generic1 : ∀S,T.∀n:counter.∀P,f,g.
+  mk_E1 S T n f g → mk_H1 S T n P P f g → mk_Ex1 S T n P f =_1 mk_Ex1 S T n P g.
+#S T n; nelim n; nnormalize;
+##[ #P f g E H; /2/;
+##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
+nqed.
+
+(* notation "∑x1,...,xn. E / H ; P" were:
+   - x1...xn are bound in E and P, H is bound in P
+   - H is an identifier that will have the type of E in P
+   - P is the proof that the two existentially quantified predicates are equal*)
+notation > "∑ list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20 
+for @{ 'Sig_gen 
+  ${ fold right @{ 'End }  rec acc @{ ('Next (λ${ident x}.${ident x}) $acc) } }
+  ${ fold right @{ $E }              rec acc @{ λ${ident x}.$acc } } 
+  ${ fold right @{ λ${ident nE}.$H } rec acc @{ λ${ident x}.$acc } }
+}.
+
+interpretation "next" 'Next x y = (Next x y).
+interpretation "end" 'End = End.
+interpretation "sig_gen" 'Sig_gen n E H = (Sig_generic  ?? n ??? E H).
+interpretation "sig_gen1" 'Sig_gen n E H = (Sig_generic1 ?? n ??? E H).
+
+(*
+nlemma test0 : ∀S:setoid. ∀P: (setoid1_of_setoid S) ⇒_1 CPROP.∀f,g:S → S.
+ (∀x:S.f x = g x) → (Ex S (λw.P (f w))) =_1 (Ex S (λw.P (g w))).
+#S P f g E; napply (∑w. E w / H ; ┼_1H); nqed.
+
+nlemma test : ∀S:setoid. ∀P: (setoid1_of_setoid S) ⇒_1 CPROP.∀f,g:S → S.
+ (∀x:S.f x = g x) → (Ex S (λw.P (f w)∧ True)) =_1 (Ex S (λw.P (g w)∧ True)).
+#S P f g E; napply (∑w. E w / H ; (┼_1H)╪_1#); nqed. 
+
+nlemma test_bound : ∀S:setoid. ∀e,f: (setoid1_of_setoid S) ⇒_1 CPROP. e = f → 
+   (Ex S (λw.e w ∧ True)) =_1 (Ex S (λw.f w ∧ True)).
+#S f g E; napply (.=_1 ∑x. E x x # / H ; (H ╪_1 #)); //; nqed.
+
+nlemma test2 : ∀S:setoid. ∀ee: (setoid1_of_setoid S) ⇒_1 (setoid1_of_setoid 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(∑w. E / E ; ((E ╪_1 #) ╪_1 #))). //; nqed.
+
+nlemma test3 : ∀S:setoid. ∀ee: (setoid1_of_setoid S) ⇒_1 (setoid1_of_setoid 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 (∑w. E / E ; ((E ╪_1 #) ╪_1 #)) ╪_1 #). //; nqed.
+*)
+  
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index ef533aab3..29e7c5ed2 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -57,12 +57,25 @@ unification hint 0 ≔ S : setoid;
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ list T.
 
+unification hint 0 ≔ SS : setoid;
+  S ≟ carr SS,
+  TT ≟ setoid1_of_setoid (LIST SS)
+(*-----------------------------------------------------------------*) ⊢ 
+  list S ≡ carr1 TT.
+
 unification hint 0 ≔ S:setoid,a,b:list S;
    R ≟ eq0 (LIST S),
    L ≟ (list S)
 (* -------------------------------------------- *) ⊢
    eq_list S a b ≡ eq_rel L R a b.
 
+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.    
+    
 notation "hvbox(hd break :: tl)"
   right associative with precedence 47
   for @{'cons $hd $tl}.
@@ -160,6 +173,8 @@ ninductive re (S: Type[0]) : Type[0] ≝
  | o: re S → re S → re S
  | k: re S → re S.
  
+(* setoid support for re *)
+ 
 nlet rec eq_re (S:Alpha) (a,b : re S) on a : CProp[0] ≝ 
   match a with
   [ z ⇒ match b with [ z ⇒ True | _ ⇒ False]
@@ -206,6 +221,44 @@ unification hint 0 ≔ A:Alpha,a,b:re A;
 (* -------------------------------------------- *) ⊢
    eq_re A a b ≡ eq_rel L R a b.
 
+nlemma c_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A) ⇒_0 (re A).
+#A; napply (mk_binary_morphism … (λs1,s2:re A. c A s1 s2));
+#a; nelim a; 
+##[##1,2: #a' b b'; ncases a'; nnormalize; /2/ by conj;
+##|#x a' b b'; ncases a'; /2/ by conj;
+##|##4,5: #r1 r2 IH1 IH2 a'; ncases a'; nnormalize; /2/ by conj;
+##|#r IH a'; ncases a'; nnormalize; /2/ by conj; ##]
+nqed.
+
+(* XXX This is the good format for hints about morphisms, fix the others *)
+unification hint 0 ≔ S:Alpha, A,B:re S;
+    MM ≟ mk_unary_morphism ??
+          (λA:re S.mk_unary_morphism ?? (λB.c ? A B) (prop1 ?? (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 ≡ c S 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. o A s1 s2));
+#a; nelim a; 
+##[##1,2: #a' b b'; ncases a'; nnormalize; /2/ by conj;
+##|#x a' b b'; ncases a'; /2/ by conj;
+##|##4,5: #r1 r2 IH1 IH2 a'; ncases a'; nnormalize; /2/ by conj;
+##|#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.o ? A B) (prop1 ?? (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 ≡ o S A B.
+
+
+(* end setoids support for re *)
+
 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
 notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
 interpretation "star" 'pk a = (k ? a).
@@ -399,176 +452,6 @@ 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).
 
-(* The caml, as some patches for it *)
-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.
-
-(* not as morphism *)
-nlemma Not_morphism : CProp[0] ⇒_1 CProp[0].
-@(λx:CProp[0].¬ x); #a b; *; #; @; /3/; nqed.
-
-unification hint 0 ≔ P : CProp[0];
-   A ≟ CPROP, 
-   B ≟ CPROP,
-   M ≟ mk_unary_morphism1 ?? (λP.¬ P) (prop11 ?? Not_morphism)
-(*------------------------*)⊢
-  fun11 A B M P ≡ ¬ P.
-
-(* XXX Ex setoid support *)
-nlemma Ex_morphism : ∀S:setoid.(S ⇒_1 CProp[0]) ⇒_1 CProp[0].
-#S; @(λP: 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 : S ⇒_1 CProp[0];
-   A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP, 
-   B ≟ CPROP,
-   M ≟ mk_unary_morphism1 ?? (λP: S ⇒_1 CProp[0].Ex S P) 
-        (prop11 ?? (Ex_morphism S))
-(*------------------------*)⊢
-  fun11 A B M P ≡ Ex S (fun11 S CPROP P).
-
-nlemma Ex_morphism_eta : ∀S:setoid.(S ⇒_1 CProp[0]) ⇒_1 CProp[0].
-#S; @(λP: 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 : S ⇒_1 CProp[0];
-   A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP, 
-   B ≟ CPROP,
-   M ≟ mk_unary_morphism1 ?? (λP: S ⇒_1 CProp[0].Ex S (λx.P x)) 
-        (prop11 ?? (Ex_morphism_eta S))
-(*------------------------*)⊢
-  fun11 A B M P ≡ Ex S (λx.fun11 S CPROP P x).
-
-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.
-
-(* couts how many Ex we are traversing *)
-ninductive counter : Type[0] ≝ 
- | End : counter 
- | Next : (bool → bool) → (* dummy arg please the notation mechanism *)
-          counter → counter. 
-
-(* to rewrite terms (live in setoid) *)
-nlet rec mk_P (S, T : setoid) (n : counter) on n ≝ 
-  match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P S T m) ].
-
-nlet rec mk_F (S, T : setoid) (n : counter) on n ≝ 
-  match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F S T m) ].
-  
-nlet rec mk_E (S, T : setoid) (n : counter) on n : ∀f,g : mk_F S T n. CProp[0] ≝ 
-  match n with 
-  [ End ⇒ λf,g:T. f = g 
-  | Next q m ⇒ λf,g: mk_F S T (Next q m). ∀x:S.mk_E S T m (f x) (g x) ].
-
-nlet rec mk_H (S, T : setoid) (n : counter) on n : 
-∀P1,P2: mk_P S T n.∀f,g : mk_F S T n. CProp[1] ≝ 
-  match n with 
-  [ End ⇒ λP1,P2:mk_P S T End.λf,g:T. f = g → P1 f =_1 P2 g 
-  | Next q m ⇒ λP1,P2: mk_P S T (Next q m).λf,g: mk_F S T (Next q m). 
-              ∀x:S.mk_H S T m (P1 x) (P2 x) (f x) (g x) ].
-
-nlet rec mk_Ex (S, T : setoid) (n : counter) on n : 
-∀P: mk_P S T n.∀f : mk_F S T n. CProp[0] ≝ 
-  match n with 
-  [ End ⇒ λP:mk_P S T End.λf:T. P f 
-  | Next q m ⇒ λP: mk_P S T (Next q m).λf: mk_F S T (Next q m). 
-              ∃x:S.mk_Ex S T m (P x) (f x) ].
-
-nlemma Sig_generic : ∀S,T.∀n:counter.∀P,f,g.
-  mk_E S T n f g → mk_H S T n P P f g → mk_Ex S T n P f =_1 mk_Ex S T n P g.
-#S T n; nelim n; nnormalize;
-##[ #P f g E H; /2/;
-##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
-nqed.
-
-(* to rewrite propositions (live in setoid1) *)
-nlet rec mk_P1 (S : setoid) (T : setoid1) (n : counter) on n ≝ 
-  match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P1 S T m) ].
-
-nlet rec mk_F1 (S : setoid) (T : setoid1) (n : counter) on n ≝ 
-  match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F1 S T m) ].
-  
-nlet rec mk_E1 (S : setoid) (T : setoid1) (n : counter) on n : ∀f,g : mk_F1 S T n. CProp[1] ≝ 
-  match n with 
-  [ End ⇒ λf,g:T. f =_1 g 
-  | Next q m ⇒ λf,g: mk_F1 S T (Next q m). ∀x:S.mk_E1 S T m (f x) (g x) ].
-
-nlet rec mk_H1 (S : setoid) (T : setoid1) (n : counter) on n : 
-∀P1,P2: mk_P1 S T n.∀f,g : mk_F1 S T n. CProp[1] ≝ 
-  match n with 
-  [ End ⇒ λP1,P2:mk_P1 S T End.λf,g:T. f = g → P1 f =_1 P2 g 
-  | Next q m ⇒ λP1,P2: mk_P1 S T (Next q m).λf,g: mk_F1 S T (Next q m). 
-              ∀x:S.mk_H1 S T m (P1 x) (P2 x) (f x) (g x) ].
-
-nlet rec mk_Ex1 (S : setoid) (T : setoid1) (n : counter) on n : 
-∀P: mk_P1 S T n.∀f : mk_F1 S T n. CProp[0] ≝ 
-  match n with 
-  [ End ⇒ λP:mk_P1 S T End.λf:T. P f 
-  | Next q m ⇒ λP: mk_P1 S T (Next q m).λf: mk_F1 S T (Next q m). 
-              ∃x:S.mk_Ex1 S T m (P x) (f x) ].
-
-nlemma Sig_generic1 : ∀S,T.∀n:counter.∀P,f,g.
-  mk_E1 S T n f g → mk_H1 S T n P P f g → mk_Ex1 S T n P f =_1 mk_Ex1 S T n P g.
-#S T n; nelim n; nnormalize;
-##[ #P f g E H; /2/;
-##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
-nqed.
-
-(* notation "∑x1,...,xn. E / H ; P" were:
-   - x1...xn are bound in E and P, H is bound in P
-   - H is an identifier that will have the type of E in P
-   - P is the proof that the two existentially quantified predicates are equal*)
-notation > "∑ list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20 
-for @{ 'Sig_gen 
-  ${ fold right @{ 'End }  rec acc @{ ('Next (λ${ident x}.${ident x}) $acc) } }
-  ${ fold right @{ $E }              rec acc @{ λ${ident x}.$acc } } 
-  ${ fold right @{ λ${ident nE}.$H } rec acc @{ λ${ident x}.$acc } }
-}.
-
-interpretation "next" 'Next x y = (Next x y).
-interpretation "end" 'End = End.
-(*interpretation "sig_gen" 'Sig_gen n E H = (Sig_generic  ?? n ??? E H).*)
-interpretation "sig_gen1" 'Sig_gen n E H = (Sig_generic1 ?? n ??? E H).
-
-nlemma test0 : ∀S:setoid. ∀P: S ⇒_1 CPROP.∀f,g:S → S.
- (∀x:S.f x = g x) → (Ex S (λw.P (f w))) =_1 (Ex S (λw.P (g w))).
-#S P f g E; napply (∑w. E w / H ; ┼_1H); nqed.
-
-nlemma test : ∀S:setoid. ∀P: S ⇒_1 CPROP.∀f,g:S → S.
- (∀x:S.f x = g x) → (Ex S (λw.P (f w)∧ True)) =_1 (Ex S (λw.P (g w)∧ True)).
-#S P f g E; napply (∑w. E w / H ; (┼_1H)╪_1#); nqed. 
-
-nlemma test_bound : ∀S:setoid. ∀e,f: S ⇒_1 CPROP. e = f → 
-   (Ex S (λw.e w ∧ True)) =_1 (Ex S (λw.f w ∧ True)).
-#S f g E; napply (.=_1 ∑x. E x x # / H ; (H ╪_1 #)); //; 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(∑w. E / E ; ((E ╪_1 #) ╪_1 #))). //; nqed.
-
-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 (∑w. E / E ; ((E ╪_1 #) ╪_1 #)) ╪_1 #). //; nqed.
-
-(* Ex setoid support end *)
-
 ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
 #S r; @(𝐋\p r); #w1 w2 E; nelim r; 
 ##[ ##1,2: /2/;
@@ -742,9 +625,6 @@ nlemma erase_star : ∀S:Alpha.∀e1:pitem S.𝐋 |e1|^* = 𝐋 |e1^*|. //; nqed
 nlemma mem_single : ∀S:setoid.∀a,b:S. a ∈ {(b)} → a = b.
 #S a b; nnormalize; /2/; nqed.
 
-notation < "[\setoid\emsp\of\emsp term 19 x]" non associative with precedence 90 for @{'mk_setoid $x}.
-interpretation "mk_setoid" 'mk_setoid x = (mk_setoid x ?).
-
 nlemma cup_sub: ∀S.∀A,B:𝛀^S.∀x. ¬ (x ∈ A) → A ∪ (B - {(x)}) = (A ∪ B) - {(x)}.
 #S A B x H; napply ext_set; #w; @; 
 ##[ *; ##[ #wa; @; ##[@;//] #H2; napply H; napply (. (mem_single ??? H2)^-1╪_1#); //]
@@ -763,30 +643,31 @@ 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; nchange in ⊢ (???%) with (|e1| · |e2|);
-
-finqui: manca · morfismo, oppure un lemma che dice che == è come Leibnitz.
-
-    nrewrite < IH1; nrewrite < IH2;  
-    nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊙ 〈e2,false〉));
-    ncases (•e1); #e3 b; ncases b; nnormalize;
-    ##[ ncases (•e2); //; ##| nrewrite > IH2; //]
-##| #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (.|e1| + .|e2|);
-    nrewrite < IH2; nrewrite < IH1;
-    nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊕ •e2));
+##[ #e1 e2 IH1 IH2;
+    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]
+    napply (.=_0 #╪_0 (IH2)); //;
+##| #e1 e2 IH1 IH2; napply (?^-1);
+    napply (.=_0 (IH1^-1)╪_0(IH2^-1));
+    nchange in match (•(e1+?)) with (?⊕?);
     ncases (•e1); ncases (•e2); //]
-##| #e IH; nchange in ⊢ (???%) with (.|e|^* ); nrewrite < IH;
-    nchange in ⊢ (??(??%)?) with (\fst (•e))^*; //; ##]
 nqed.
 
-nlemma eta_lp : ∀S.∀p:pre S.𝐋\p p = 𝐋\p 〈\fst p, \snd p〉.
+nlemma eta_lp : ∀S:Alpha.∀p:pre S. 𝐋\p p = 𝐋\p 〈\fst p, \snd p〉.
 #S p; ncases p; //; nqed.
 
-nlemma epsilon_dot: ∀S.∀p:word S → Prop. {[]} · p = p. 
-#S e; napply extP; #w; nnormalize; @; ##[##2: #Hw; @[]; @w; /3/; ##]
-*; #w1; *; #w2; *; *; #defw defw1 Hw2; nrewrite < defw; nrewrite < defw1;
+(* ext_carr non applica *)
+nlemma epsilon_dot: ∀S:Alpha.∀p:Elang S. {[]} · (ext_carr ? p) = p. 
+#S e; napply ext_set; #w; @; ##[##2: #Hw; @[]; @w; @; //; @; //; napply #; (* XXX auto *) ##]
+*; #w1; *; #w2; *; *; #defw defw1 Hw2; 
+napply (. defw╪_1#);
+napply (. (defw1^-1 ╪_0 #)╪_1#); (* manca @ morfismo *)
 napply Hw2; nqed.
 
+STOP
+
 (* theorem 16: 1 → 3 *)
 nlemma odot_dot_aux : ∀S.∀e1,e2: pre S.
       𝐋\p (•(\fst e2)) =  𝐋\p (\fst e2) ∪ 𝐋 .|\fst e2| → 
diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index e593ea7d5..376edc0ce 100644
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -28,6 +28,9 @@ unification hint 0 ≔ R : setoid;
 (* ---------------------------------------- *) ⊢ 
    setoid ≡ force1 ? MR lock.
 
+notation < "[\setoid\ensp\of term 19 x]" non associative with precedence 90 for @{'mk_setoid $x}.
+interpretation "mk_setoid" 'mk_setoid x = (mk_setoid x ?).
+
 interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
 
 notation > "hvbox(a break =_0 b)" non associative with precedence 45
@@ -80,7 +83,7 @@ nlemma unary_morph_eq: ∀A,B.∀f,g:A ⇒_0 B. (∀x. f x = g x) → f = g.
 nlemma mk_binary_morphism:
  ∀A,B,C: setoid. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') →
   A ⇒_0 (unary_morph_setoid B C).
- #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y]
+ #A; #B; #C; #f; #H; @; ##[ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y]
  /2/.
 nqed.
 
@@ -96,10 +99,10 @@ 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)
+   R ≟ mk_unary_morphism ?? (composition ??? f g)
         (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
  (* -------------------------------------------------------------------- *) ⊢
-                              fun1 ?? R ≡ (composition … f g).
+                              fun1 ?? R ≡ (composition ??? f 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 4ab57d568..48b7d3fcc 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -27,10 +27,21 @@ unification hint 0 ≔ R : setoid1;
 (* ---------------------------------------- *) ⊢ 
    setoid1 ≡ force2 ? MR lock.
 
+notation < "[\setoid1\ensp\of term 19 x]" non associative with precedence 90 for @{'mk_setoid1 $x}.
+interpretation "mk_setoid1" 'mk_setoid1 x = (mk_setoid1 x ?).
+
+(* da capire se mettere come coercion *)
 ndefinition setoid1_of_setoid: setoid → setoid1.
  #s; @ (carr s); @ (eq0…) (refl…) (sym…) (trans…);
 nqed.
 
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type2".
+unification hint 0 ≔ A,x,y
+(*-----------------------------------------------*) ⊢
+   eq_rel ? (eq0 A) x y ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) x y.
+(* XXX capire come mai questa hint non funziona se porto su (setoid1_of_setoid A) *)
+
 interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
 interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
 
@@ -102,10 +113,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 ??? f g)
         (prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
  (* -------------------------------------------------------------------- *) ⊢
-                              fun11 ?? R ≡ (composition1 … f g).
+                              fun11 ?? R ≡ (composition1 ??? f 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 dcb740921..aae969ed2 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -34,6 +34,10 @@ interpretation "intersect" 'intersects U V = (intersect ? U V).
 ndefinition union ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∨ x ∈ V }.
 interpretation "union" 'union U V = (union ? U V).
 
+ndefinition substract ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ ¬ x ∈ V }.
+interpretation "substract" 'minus U V = (substract ? U V).
+
+
 ndefinition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ x ∈ f i }.
 
 ndefinition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }.
@@ -55,6 +59,9 @@ nqed.
 
 include "sets/setoids1.ma".
 
+ndefinition singleton ≝ λA:setoid.λa:A.{ x | a = x }.
+interpretation "singl" 'singl a = (singleton ? a).
+
 (* this has to be declared here, so that it is combined with carr *)
 ncoercion full_set : ∀A:Type[0]. Ω^A ≝ full_set on A: Type[0] to (Ω^?).
 
@@ -138,13 +145,7 @@ nlemma subseteq_is_morph: ∀A.  𝛀^A ⇒_1 𝛀^A ⇒_1 CPROP.
  #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,x,y
-(*-----------------------------------------------*) ⊢
-   eq_rel ? (eq0 A) x y ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) x y.
-   
-(* XXX capire come mai questa hint non funziona se porto su (setoid1_of_setoid A) *)
-
+(* 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‡#); nassumption;
@@ -195,6 +196,8 @@ unification hint 1 ≔
    (* ------------------------------------------------------*) ⊢ 
             ext_carr AA (R B C) ≡ intersect A BB CC.
 
+
+(* hints for ∩ *)
 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;
@@ -245,6 +248,92 @@ unification hint 1 ≔
 (*------------------------------------------------------*) ⊢
    ext_carr AA (R B C) ≡ union A BB CC.
 
+
+(* hints for - *)
+nlemma substract_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;
+nchange in match (x ∈ (A1 - B1)) with (?∧?);
+napply (.= (set_ext ??? EA x)‡#); @; *; #H H1; @; //; #H2; napply H1;
+##[ napply (. (set_ext ??? EB x)); ##| napply (. (set_ext ??? EB^-1 x)); ##] //;
+nqed.
+
+nlemma substract_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
+ #S A B; @ (A - B); #x y Exy; @; *; #H1 H2; @; ##[##2,4: #H3; napply H2]
+##[##1,4: napply (. Exy╪_1#); // ##|##2,3: napply (. Exy^-1╪_1#); //]
+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 ≔ S:Type[0], A,B:Ω^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.
+   
+nlemma substract_is_ext_morph:∀A.𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A.
+#A; napply (mk_binary_morphism1 …  (substract_is_ext …));
+#x1 x2 y1 y2 Ex Ey; napply (prop11 … (substract_is_morph A)); nassumption.
+nqed.
+            
+unification hint 1 ≔
+  AA : setoid, B,C : 𝛀^AA;
+  A ≟ carr 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))) ,
+   BB ≟ (ext_carr ? B),
+   CC ≟ (ext_carr ? C)
+(*------------------------------------------------------*) ⊢
+   ext_carr AA (R B C) ≡ substract A BB CC.
+
+(* hints for {x} *)
+nlemma single_is_morph : ∀A:setoid. (setoid1_of_setoid A) ⇒_1 Ω^A.
+#X; @; ##[ napply (λx.{(x)}); ##] 
+#a b E; napply ext_set; #x; @; #H; /3/; nqed.
+
+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;
+   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;
+  MM ≟ mk_unary_morphism1 ?? 
+         (λa:setoid1_of_setoid A.{(a)}) (prop11 ?? (single_is_morph A))
+(*--------------------------------------------------------------------------*) ⊢
+   fun11 ?? 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;
+  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.
+
+
+
+
+
+
 (*
 alias symbol "hint_decl" = "hint_decl_Type2".
 unification hint 0 ≔
-- 
2.39.2