From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Tue, 2 Mar 2010 16:19:18 +0000 (+0000)
Subject: Some integrations to the ng library.
X-Git-Tag: make_still_working~3020
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=edccb29109d07b54b48230a280f4351ed042dd9f;p=helm.git

Some integrations to the ng library.
---

diff --git a/helm/software/matita/nlibrary/arithmetics/Z.ma b/helm/software/matita/nlibrary/arithmetics/Z.ma
new file mode 100644
index 000000000..7a0f7f080
--- /dev/null
+++ b/helm/software/matita/nlibrary/arithmetics/Z.ma
@@ -0,0 +1,631 @@
+(**************************************************************************)
+(*       ___	                                                            *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "arithmetics/nat.ma".
+
+ninductive Z : Type ≝
+  OZ : Z
+| pos : nat → Z
+| neg : nat → Z.
+
+interpretation "Integers" 'Z = Z.
+
+ndefinition Z_of_nat ≝
+λn. match n with
+[ O ⇒ OZ 
+| S n ⇒ pos n].
+
+ncoercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z.
+
+ndefinition neg_Z_of_nat \def
+λn. match n with
+[ O ⇒ OZ 
+| S n ⇒ neg n].
+
+nlemma pos_n_eq_S_n : ∀n : nat.pos n = S n.
+//.
+nqed.
+
+ndefinition abs ≝
+λz.match z with 
+[ OZ ⇒ O
+| pos n ⇒ S n
+| neg n ⇒ S n].
+
+ndefinition OZ_test ≝
+λz.match z with 
+[ OZ ⇒ true
+| pos _ ⇒ false
+| neg _ ⇒ false].
+
+ntheorem OZ_test_to_Prop : ∀z:Z.
+  match OZ_test z with
+  [true ⇒ z=OZ 
+  |false ⇒ z ≠ OZ].
+#z;ncases z
+##[napply refl
+##|##*:#z1;#H;ndestruct]
+nqed.
+
+(* discrimination *)
+ntheorem injective_pos: injective nat Z pos.
+#n;#m;#H;ndestruct;//;
+nqed.
+
+(* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
+\def injective_pos. *)
+
+ntheorem injective_neg: injective nat Z neg.
+#n;#m;#H;ndestruct;//;
+nqed.
+
+(* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
+\def injective_neg. *)
+
+ntheorem not_eq_OZ_pos: ∀n:nat. OZ ≠ pos n.
+#n;#H;ndestruct;
+nqed.
+
+ntheorem not_eq_OZ_neg :∀n:nat. OZ ≠ neg n.
+#n;#H;ndestruct;
+nqed.
+
+ntheorem not_eq_pos_neg : ∀n,m:nat. pos n ≠ neg m.
+#n;#m;#H;ndestruct;
+nqed.
+
+ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
+#x;#y;ncases x;
+##[ncases y;
+   ##[@;//
+   ##|##*:#n;@2;#H;ndestruct]
+##|#n;ncases y;
+   ##[@2;#H;ndestruct;
+   ##|#m;ncases (decidable_eq_nat n m);#H;
+      ##[nrewrite > H;@;//
+      ##|@2;#H2;napply H;ndestruct;//]
+   ##|#m;@2;#H;ndestruct]
+##|#n;ncases y;
+   ##[@2;#H;ndestruct;
+   ##|#m;@2;#H;ndestruct
+   ##|#m;ncases (decidable_eq_nat n m);#H;
+      ##[nrewrite > H;@;//
+      ##|@2;#H2;napply H;ndestruct;//]##]##]
+nqed.
+
+ndefinition Zsucc ≝
+λz. match z with
+[ OZ ⇒ pos O
+| pos n ⇒ pos (S n)
+| neg n ⇒
+	  match n with
+	  [ O ⇒ OZ
+	  | S p ⇒ neg p]].
+
+ndefinition Zpred ≝
+λz. match z with
+[ OZ ⇒ neg O
+| pos n ⇒
+	  match n with
+	  [ O ⇒ OZ
+	  | S p ⇒ pos p]
+| neg n ⇒ neg (S n)].
+
+ntheorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z.
+#z;ncases z;
+##[##1,2://
+##|#n;ncases n;//]
+nqed.
+
+ntheorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z.
+#z;ncases z
+##[##2:#n;ncases n;//
+##|##*://]
+nqed.
+
+ndefinition Zle : Z → Z → Prop ≝
+λx,y:Z.
+  match x with
+  [ OZ ⇒ 
+    match y with 
+    [ OZ ⇒ True
+    | pos m ⇒ True
+    | neg m ⇒ False ]
+  | pos n ⇒
+    match y with 
+    [ OZ ⇒ False
+    | pos m ⇒ n ≤ m
+    | neg m ⇒ False ]
+  | neg n ⇒
+    match y with 
+    [ OZ ⇒ True
+    | pos m ⇒ True
+    | neg m ⇒ m ≤ n ]].
+
+interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
+interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
+
+ndefinition Zlt : Z → Z → Prop ≝
+λx,y:Z.
+  match x with
+  [ OZ ⇒
+    match y with 
+    [ OZ ⇒ False
+    | pos m ⇒ True
+    | neg m ⇒ False ]
+  | pos n ⇒
+    match y with 
+    [ OZ ⇒ False
+    | pos m ⇒ n<m
+    | neg m ⇒ False ]
+  | neg n ⇒
+    match y with 
+    [ OZ ⇒ True
+    | pos m ⇒ True
+    | neg m ⇒ m<n ]].
+    
+interpretation "integer 'less than'" 'lt x y = (Zlt x y).
+interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
+
+ntheorem irreflexive_Zlt: irreflexive Z Zlt.
+#x;ncases x
+##[//
+##|##*:#n;napply (not_le_Sn_n n) (* XXX: auto?? *)]
+nqed.
+
+(* transitivity *)
+ntheorem transitive_Zle : transitive Z Zle.
+#x;#y;#z;ncases x
+##[ncases y
+   ##[//
+   ##|##*:#n;ncases z;//]
+##|#n;ncases y
+   ##[#H;ncases H
+   ##|(*##*:#m;#Hl;ncases z;//;*)
+      #m;#Hl;ncases z;//;#p;#Hr;
+      napply (transitive_le n m p);//; (* XXX: auto??? *)
+   ##|#m;#Hl;ncases Hl]
+##|#n;ncases y
+   ##[#Hl;ncases z
+      ##[##1,2://
+      ##|#m;#Hr;ncases Hr]
+   ##|#m;#Hl;ncases z;
+      ##[##1,2://
+      ##|#p;#Hr;ncases Hr]
+   ##|#m;#Hl;ncases z;//;#p;#Hr;
+      napply (transitive_le p m n);//; (* XXX: auto??? *) ##]
+nqed.
+
+(* variant trans_Zle: transitive Z Zle
+\def transitive_Zle.*)
+
+ntheorem transitive_Zlt: transitive Z Zlt.
+#x;#y;#z;ncases x
+##[ncases y
+   ##[//
+   ##|#n;ncases z
+      ##[#_;#Hr;ncases Hr
+      ##|//
+      ##|#m;#_;#Hr;ncases Hr]
+   ##|#n;#Hl;ncases Hl]
+##|#n;ncases y
+   ##[#Hl;ncases Hl
+   ##|#m;ncases z
+      ##[//
+      ##|#p;napply transitive_lt (* XXX: auto??? *) 
+      ##|//##]
+   ##|#m;#Hl;ncases Hl]
+##|#n;ncases y
+   ##[ncases z;
+      ##[##1,2://
+      ##|#m;#_;#Hr;ncases Hr]
+   ##|#m;ncases z;
+      ##[##1,2://
+      ##|#p;#_;#Hr;ncases Hr]
+   ##|#m;ncases z
+      ##[##1,2://
+      ##|#p;#Hl;#Hr;napply (transitive_lt … Hr Hl)]
+   ##]
+##]
+nqed.     
+
+(* variant trans_Zlt: transitive Z Zlt
+\def transitive_Zlt.
+theorem irrefl_Zlt: irreflexive Z Zlt
+\def irreflexive_Zlt.*)
+
+ntheorem Zlt_neg_neg_to_lt: 
+  ∀n,m:nat. neg n < neg m → m < n.
+//;
+nqed.
+
+ntheorem lt_to_Zlt_neg_neg: ∀n,m:nat.m < n → neg n < neg m. 
+//;
+nqed.
+
+ntheorem Zlt_pos_pos_to_lt: 
+  ∀n,m:nat. pos n < pos m → n < m.
+//;
+nqed.
+
+ntheorem lt_to_Zlt_pos_pos: ∀n,m:nat.n < m → pos n < pos m. 
+//;
+nqed.
+
+ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
+#x;#y;ncases x
+##[ncases y
+   ##[#H;ncases H
+   ##|//;
+   ##|#p;#H;ncases H]
+##|#n;ncases y
+   ##[#H;ncases H
+   ##|#p;nnormalize;//
+   ##|#p;#H;ncases H]
+##|#n;ncases y
+   ##[##1,2:ncases n;//
+   ##|#p;ncases n;nnormalize;
+      ##[napply not_le_Sn_O (* XXX: auto? *)
+      ##|#m;napply le_S_S_to_le (* XXX: auto? *)]
+   ##]
+##]
+nqed.
+
+(*** COMPARE ***)
+
+(* boolean equality *)
+ndefinition eqZb : Z → Z → bool ≝
+λx,y:Z.
+  match x with
+  [ OZ ⇒
+      match y with
+        [ OZ ⇒ true
+        | pos q ⇒ false
+        | neg q ⇒ false]
+  | pos p ⇒
+      match y with
+        [ OZ ⇒ false
+        | pos q ⇒ eqb p q
+        | neg q ⇒ false]     
+  | neg p ⇒
+      match y with
+        [ OZ ⇒ false
+        | pos q ⇒ false
+        | neg q ⇒ eqb p q]].
+
+ntheorem eqZb_to_Prop: 
+  ∀x,y:Z. 
+    match eqZb x y with
+    [ true ⇒ x=y
+    | false ⇒ x ≠ y].
+#x;#y;ncases x
+##[ncases y;
+   ##[//
+   ##|napply not_eq_OZ_pos (* XXX: auto? *)
+   ##|napply not_eq_OZ_neg (* XXX: auto? *)]
+##|#n;ncases y;
+   ##[#H;napply not_eq_OZ_pos;//;
+   ##|#m;napply eqb_elim;
+      ##[//
+      ##|#H;#H2;napply H;ndestruct;//]
+   ##|#m;napply not_eq_pos_neg]
+##|#n;ncases y
+   ##[#H;napply not_eq_OZ_neg;//;
+   ##|#m;#H;ndestruct
+   ##|#m;napply eqb_elim;
+      ##[//
+      ##|#H;#H2;napply H;ndestruct;//]
+   ##]
+##]
+nqed.
+
+ntheorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop.
+  (x=y → P true) → (x ≠ y → P false) → P (eqZb x y).
+#x;#y;#P;#HP1;#HP2;
+ncut 
+(match (eqZb x y) with
+[ true ⇒ x=y
+| false ⇒ x ≠ y] → P (eqZb x y))
+##[ncases (eqZb x y);nnormalize; (* XXX: auto?? *)
+   ##[napply HP1
+   ##|napply HP2]
+##|#Hcut;napply Hcut;napply eqZb_to_Prop]
+nqed.
+
+ndefinition Z_compare : Z → Z → compare ≝
+λx,y:Z.
+  match x with
+  [ OZ ⇒
+    match y with 
+    [ OZ ⇒ EQ
+    | pos m ⇒ LT
+    | neg m ⇒ GT ]
+  | pos n ⇒
+    match y with 
+    [ OZ ⇒ GT
+    | pos m ⇒ nat_compare n m
+    | neg m ⇒ GT]
+  | neg n ⇒ 
+    match y with 
+    [ OZ ⇒ LT
+    | pos m ⇒ LT
+    | neg m ⇒ nat_compare m n ]].
+
+ntheorem Z_compare_to_Prop : 
+∀x,y:Z. match (Z_compare x y) with
+[ LT ⇒ x < y
+| EQ ⇒ x=y
+| GT ⇒ y < x]. 
+#x;#y;nelim x
+##[nelim y;//;
+##|nelim y
+   ##[##1,3://
+   ##|#n;#m;nnormalize;
+      ncut (match (nat_compare m n) with
+      [ LT ⇒ m < n
+      | EQ ⇒ m = n
+      | GT ⇒ n < m ] →
+      match (nat_compare m n) with
+      [ LT ⇒ S m  ≤ n
+      | EQ ⇒ pos m = pos n
+      | GT ⇒ S n  ≤ m])
+      ##[ncases (nat_compare m n);//
+      ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
+   ##]
+##|nelim y
+   ##[#n;//
+   ##|nnormalize;//
+   ##|nnormalize;#n;#m;
+      ncut (match (nat_compare n m) with
+        [ LT ⇒ n < m
+        | EQ ⇒ n = m
+        | GT ⇒ m < n] →
+      match (nat_compare n m) with
+      [ LT ⇒ S n ≤ m
+      | EQ ⇒ neg m = neg n
+      | GT ⇒ S m ≤ n])
+      ##[ncases (nat_compare n m);//
+      ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
+   ##]
+##]
+nqed.
+
+ndefinition Zplus : Z → Z → Z ≝
+  λx,y. match x with
+    [ OZ ⇒ y
+    | pos m ⇒
+        match y with
+         [ OZ ⇒ x
+         | pos n ⇒ (pos (pred ((S m)+(S n))))
+         | neg n ⇒ 
+              match nat_compare m n with
+                [ LT ⇒ (neg (pred (n-m)))
+                | EQ ⇒ OZ
+                | GT ⇒ (pos (pred (m-n)))] ]
+    | neg m ⇒
+        match y with
+         [ OZ ⇒ x
+         | pos n ⇒
+              match nat_compare m n with
+                [ LT ⇒ (pos (pred (n-m)))
+                | EQ ⇒ OZ
+                | GT ⇒ (neg (pred (m-n)))]     
+         | neg n ⇒ (neg (pred ((S m)+(S n))))] ].
+
+interpretation "integer plus" 'plus x y = (Zplus x y).
+
+ntheorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m.
+#n;#m;ncases n
+##[//
+##|#p;ncases m
+   ##[nnormalize;//
+   ##|//]
+nqed.
+
+ntheorem Zplus_z_OZ: ∀z:Z. z+OZ = z.
+#z;ncases z;//;
+nqed.
+
+(* theorem symmetric_Zplus: symmetric Z Zplus. *)
+
+ntheorem sym_Zplus : ∀x,y:Z. x+y = y+x.
+#x;#y;ncases x;
+##[nrewrite > (Zplus_z_OZ ?) (*XXX*);//
+##|#p;ncases y
+   ##[//
+   ##|nnormalize;//
+   ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*);
+      ncases (nat_compare q p);//]
+##|#p;ncases y
+   ##[//;
+   ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*);
+      ncases (nat_compare q p);//
+   ##|nnormalize;//]
+##]
+nqed.
+
+ntheorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg O)+z.
+#z;ncases z
+##[//
+##|##*:#n;ncases n;//]
+nqed.
+
+ntheorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos O)+z.
+#z;ncases z
+##[//
+##|##*:#n;ncases n;//]
+nqed.
+
+ntheorem Zplus_pos_pos:
+  ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
+#n;#m;ncases n
+##[ncases m;//
+##|#p;ncases m
+   ##[nnormalize;
+      nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_O ?); (* XXX yet again *)
+      //
+   ##|#q;nnormalize;nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_Sm ??);//]
+##]
+nqed.
+
+ntheorem Zplus_pos_neg:
+  ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
+//;
+nqed.
+
+ntheorem Zplus_neg_pos :
+  ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
+#n;#m;ncases n;ncases m;//;
+nqed.
+
+ntheorem Zplus_neg_neg:
+  ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
+#n;#m;ncases n
+##[ncases m;//
+##|#p;ncases m;nnormalize;
+   ##[nrewrite > (plus_n_Sm ??);//
+   ##|#q;nrewrite > (plus_n_Sm ??);//]
+##]
+nqed.
+
+ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
+#x;#y;ncases x
+##[ncases y
+   ##[//
+   ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
+   ##|//]
+##|ncases y;//
+##|ncases y
+   ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
+      nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
+   ##|##*://]
+nqed.
+
+ntheorem Zplus_Zsucc_pos_pos : 
+  ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
+//;
+nqed.
+
+ntheorem Zplus_Zsucc_pos_neg: 
+  ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
+#n;#m;
+napply (nat_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
+##[#n1;nelim n1
+   ##[//
+   ##|#n2;#IH;nelim n2;//]
+##|//
+##|#n1;#m1;#IH;nrewrite < (Zplus_pos_neg ? m1);nelim IH;//]
+nqed.
+
+ntheorem Zplus_Zsucc_neg_neg : 
+  ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
+#n;#m;
+napply (nat_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
+##[#n1;nelim n1
+   ##[//
+   ##|#n2;#IH;nelim n2;//]
+##|##*://]
+nqed.
+
+ntheorem Zplus_Zsucc_neg_pos: 
+  ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
+#n;#m;
+napply (nat_elim2 (λn,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)))
+##[#n1;nelim n1
+   ##[//
+   ##|#n2;#IH;nelim n2;//]
+##|//
+##|#n1;#m1;#IH;nrewrite < IH;nrewrite < (Zplus_neg_pos ? (S m1));//]
+nqed.
+
+ntheorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y).
+#x;#y;ncases x
+##[ncases y;//;#n;nnormalize;ncases n;//;
+##|##*:#n;ncases y;//]
+nqed.
+
+ntheorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y).
+#x;#y;ncut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y))
+##[nrewrite > (Zsucc_Zpred ?);//
+##|#Hcut;nrewrite > Hcut;nrewrite > (Zplus_Zsucc ??);//]
+nqed.
+
+ntheorem associative_Zplus: associative Z Zplus.
+(* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
+#x;#y;#z;ncases x
+##[//
+##|#n;nelim n
+   ##[nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite < (Zsucc_Zplus_pos_O ?);//;
+   ##|#n1;#IH;
+      nrewrite > (Zplus_Zsucc (pos n1) ?);nrewrite > (Zplus_Zsucc (pos n1) ?);
+      nrewrite > (Zplus_Zsucc ((pos n1)+y) ?);//]
+##|#n;nelim n
+   ##[nrewrite < (Zpred_Zplus_neg_O (y+z));nrewrite < (Zpred_Zplus_neg_O y);//;
+   ##|#n1;#IH;
+      nrewrite > (Zplus_Zpred (neg n1) ?);nrewrite > (Zplus_Zpred (neg n1) ?);
+      nrewrite > (Zplus_Zpred ((neg n1)+y) ?);//]
+##]
+nqed.
+
+(* variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
+\def associative_Zplus. *)
+
+(* Zopp *)
+ndefinition Zopp : Z → Z ≝
+  λx:Z. match x with
+  [ OZ ⇒ OZ
+  | pos n ⇒ neg n
+  | neg n ⇒ pos n ].
+
+interpretation "integer unary minus" 'uminus x = (Zopp x).
+
+ntheorem eq_OZ_Zopp_OZ : OZ = (- OZ).
+//;
+nqed.
+
+ntheorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y.
+#x;#y;ncases x
+##[ncases y;//
+##|##*:#n;ncases y;//;#m;nnormalize;napply nat_compare_elim;nnormalize;//]
+nqed.
+
+ntheorem Zopp_Zopp: ∀x:Z. --x = x.
+#x;ncases x;//;
+nqed.
+
+ntheorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ.
+#x;ncases x
+##[//
+##|##*:#n;nnormalize;nrewrite > (nat_compare_n_n ?);//]
+nqed.
+
+ntheorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).
+#x;#z;#y;#H;
+nrewrite < (Zplus_z_OZ z);nrewrite < (Zplus_z_OZ y);
+nrewrite < (Zplus_Zopp x);
+nrewrite < (associative_Zplus ???);nrewrite < (associative_Zplus ???);
+//;
+nqed.
+
+ntheorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).
+#x;#z;#y;#H;
+napply (injective_Zplus_l x);
+nrewrite < (sym_Zplus ??);
+//;
+nqed.
+
+(* minus *)
+ndefinition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y).
+
+interpretation "integer minus" 'minus x y = (Zminus x y).
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index 120a0bb16..25745e370 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -1135,3 +1135,99 @@ nqed.
 ntheorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
 #n; #m; #Hltb; napply lt_to_leb_false; /2/;
 nqed. *)
+
+ninductive compare : Type[0] ≝
+| LT : compare
+| EQ : compare
+| GT : compare.
+
+ndefinition compare_invert: compare → compare ≝
+  λc.match c with
+      [ LT ⇒ GT
+      | EQ ⇒ EQ
+      | GT ⇒ LT ].
+
+nlet rec nat_compare n m: compare ≝
+match n with
+[ O ⇒ match m with 
+      [ O ⇒ EQ
+      | (S q) ⇒ LT ]
+| S p ⇒ match m with 
+      [ O ⇒ GT
+      | S q ⇒ nat_compare p q]].
+
+ntheorem nat_compare_n_n: ∀n. nat_compare n n = EQ.
+#n;nelim n
+##[//
+##|#m;#IH;nnormalize;//]
+nqed.
+
+ntheorem nat_compare_S_S: ∀n,m:nat.nat_compare n m = nat_compare (S n) (S m).
+//;
+nqed.
+
+ntheorem nat_compare_pred_pred: 
+  ∀n,m.O < n → O < m → nat_compare n m = nat_compare (pred n) (pred m).
+#n;#m;#Hn;#Hm;
+napply (lt_O_n_elim n Hn);
+napply (lt_O_n_elim m Hm);
+#p;#q;//;
+nqed.
+
+ntheorem nat_compare_to_Prop: 
+  ∀n,m.match (nat_compare n m) with
+    [ LT ⇒ n < m
+    | EQ ⇒ n = m
+    | GT ⇒ m < n ].
+#n;#m;
+napply (nat_elim2 (λn,m.match (nat_compare n m) with
+  [ LT ⇒ n < m
+  | EQ ⇒ n = m
+  | GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *)
+##[##1,2:#n1;ncases n1;//;
+##|#n1;#m1;nnormalize;ncases (nat_compare n1 m1);
+   ##[##1,3:nnormalize;#IH;napply le_S_S;//;
+   ##|nnormalize;#IH;nrewrite > IH;//]
+nqed.
+
+ntheorem nat_compare_n_m_m_n: 
+  ∀n,m:nat.nat_compare n m = compare_invert (nat_compare m n).
+#n;#m;
+napply (nat_elim2 (λn,m. nat_compare n m = compare_invert (nat_compare m n)))
+##[##1,2:#n1;ncases n1;//;
+##|#n1;#m1;#IH;nnormalize;napply IH]
+nqed.
+     
+ntheorem nat_compare_elim : 
+  ∀n,m. ∀P:compare → Prop.
+    (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (nat_compare n m).
+#n;#m;#P;#Hlt;#Heq;#Hgt;
+ncut (match (nat_compare n m) with
+    [ LT ⇒ n < m
+    | EQ ⇒ n=m
+    | GT ⇒ m < n] →
+  P (nat_compare n m))
+##[ncases (nat_compare n m);
+   ##[napply Hlt
+   ##|napply Heq
+   ##|napply Hgt]
+##|#Hcut;napply Hcut;//;
+nqed.
+
+ninductive cmp_cases (n,m:nat) : CProp[0] ≝
+  | cmp_le : n ≤ m → cmp_cases n m
+  | cmp_gt : m < n → cmp_cases n m.
+
+ntheorem lt_to_le : ∀n,m:nat. n < m → n ≤ m.
+#n;#m;#H;nelim H
+##[//
+##|/2/]
+nqed.
+
+nlemma cmp_nat: ∀n,m.cmp_cases n m.
+#n;#m; nlapply (nat_compare_to_Prop n m);
+ncases (nat_compare n m);#H
+##[@;napply lt_to_le;//
+##|@;//
+##|@2;//]
+nqed.
diff --git a/helm/software/matita/nlibrary/datatypes/list.ma b/helm/software/matita/nlibrary/datatypes/list.ma
new file mode 100644
index 000000000..0e1337725
--- /dev/null
+++ b/helm/software/matita/nlibrary/datatypes/list.ma
@@ -0,0 +1,333 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "arithmetics/nat.ma".
+
+ninductive list (A:Type[0]) : Type[0] ≝ 
+  | nil: list A
+  | cons: A -> list A -> list A.
+
+notation "hvbox(hd break :: tl)"
+  right associative with precedence 47
+  for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+  non associative with precedence 90
+  for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+  right associative with precedence 47
+  for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+
+ntheorem nil_cons:
+  ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
+#A;#l;#a;#H;ndestruct;
+nqed.
+
+nlet rec id_list A (l: list A) on l ≝ 
+  match l with
+  [ nil ⇒ []
+  | cons hd tl ⇒ hd :: id_list A tl ].
+
+nlet rec append A (l1: list A) l2 on l1 ≝ 
+  match l1 with
+  [ nil ⇒ l2
+  | cons hd tl ⇒ hd :: append A tl l2 ].
+
+ndefinition tail ≝ λA:Type[0].λl:list A.
+  match l with
+  [ nil ⇒  []
+  | cons hd tl ⇒  tl].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
+#A;#l;nelim l;//;
+#a;#l1;#IH;nnormalize;//;
+nqed.
+
+ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
+#A;#x;#y;#z;nelim x
+##[//
+##|#a;#x1;#H;nnormalize;//]
+nqed.
+
+ntheorem cons_append_commute:
+  ∀A:Type[0].∀l1,l2:list A.∀a:A.
+    a :: (l1 @ l2) = (a :: l1) @ l2.
+//;
+nqed.
+
+nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
+#A;#a;#l;#l1;nrewrite > (associative_append ????);//;
+nqed.
+
+(*ninductive permutation (A:Type) : list A -> list A -> Prop \def
+  | refl : \forall l:list A. permutation ? l l
+  | swap : \forall l:list A. \forall x,y:A. 
+              permutation ? (x :: y :: l) (y :: x :: l)
+  | trans : \forall l1,l2,l3:list A.
+              permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3
+with permut1 : list A -> list A -> Prop \def
+  | step : \forall l1,l2:list A. \forall x,y:A. 
+      permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*)
+
+(*
+
+definition x1 \def S O.
+definition x2 \def S x1.
+definition x3 \def S x2.
+   
+theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
+  apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?).
+  apply refl.
+  apply (step ? (x1::[]) [] x2 x3).
+  qed. 
+
+theorem nil_append_nil_both:
+  \forall A:Type.\forall l1,l2:list A.
+    l1 @ l2 = [] \to l1 = [] \land l2 = [].
+
+theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. 
+reflexivity.
+qed.
+
+theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
+simplify.
+reflexivity.
+qed.
+
+*)
+
+nlet rec nth A l d n on n ≝
+  match n with
+  [ O ⇒ match l with
+        [ nil ⇒ d
+        | cons (x : A) _ ⇒ x ]
+  | S n' ⇒ nth A (tail ? l) d n'].
+
+nlet rec map A B f l on l ≝
+  match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ]. 
+
+nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝ 
+  match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
+   
+ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
+
+ndefinition filter ≝ 
+  λT:Type[0].λl:list T.λp:T → bool.
+  foldr T (list T) 
+    (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
+
+ndefinition iota : nat → nat → list nat ≝
+  λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
+  
+(* ### induction principle for functions visiting 2 lists in parallel *)
+nlemma list_ind2 : 
+  ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
+  length ? l1 = length ? l2 →
+  (P (nil ?) (nil ?)) → 
+  (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → 
+  P l1 l2.
+#T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons;
+ngeneralize in match Hl; ngeneralize in match l2;
+nelim l1
+##[#l2;ncases l2;//;
+   nnormalize;#t2;#tl2;#H;ndestruct;
+##|#t1;#tl1;#IH;#l2;ncases l2
+   ##[nnormalize;#H;ndestruct
+   ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//]
+##]
+nqed.
+
+nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+#A;#B;#f;#g;#l;#Efg;
+nelim l; nnormalize;//;
+nqed.
+
+nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l.
+#A;#l;#p;nelim l;nnormalize
+##[//
+##|#a;#tl;#IH;ncases (p a);nnormalize;
+   ##[napply le_S_S;//;
+   ##|@2;//]
+##]
+nqed.
+
+nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
+#A;#l;#m;nelim l;
+##[//
+##|#H;#tl;#IH;nnormalize;nrewrite < IH;//]
+nqed.
+
+ninductive in_list (A:Type): A → (list A) → Prop ≝
+| in_list_head : ∀ x,l.(in_list A x (x::l))
+| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
+
+ndefinition incl : \forall A.(list A) \to (list A) \to Prop \def
+  \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
+  
+notation "hvbox(a break ∉ b)" non associative with precedence 45
+for @{ 'notmem $a $b }. 
+  
+interpretation "list member" 'mem x l = (in_list ? x l).
+interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
+interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
+  
+naxiom not_in_list_nil : \forall A,x.\lnot in_list A x [].
+(*intros.unfold.intro.inversion H
+  [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
+  |intros;destruct H4]
+qed.*)
+
+naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
+                          x = a \lor in_list A x l.
+(*intros;inversion H;intros
+  [destruct H2;left;reflexivity
+  |destruct H4;right;assumption]
+qed.*)
+
+naxiom in_list_tail : \forall l,x,y.
+      in_list nat x (y::l) \to x \neq y \to in_list nat x l.
+(*intros 4;elim (in_list_cons_case ? ? ? ? H)
+  [elim (H2 H1)
+  |assumption]
+qed.*)
+
+naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
+(*intros;elim (in_list_cons_case ? ? ? ? H)
+  [assumption
+  |elim (not_in_list_nil ? ? H1)]
+qed.*)
+
+naxiom in_list_to_in_list_append_l: \forall A.\forall x:A.
+\forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
+(*intros.
+elim H;simplify
+  [apply in_list_head
+  |apply in_list_cons;assumption
+  ]
+qed.*)
+
+naxiom in_list_to_in_list_append_r: \forall A.\forall x:A.
+\forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
+(*intros 3.
+elim l1;simplify
+  [assumption
+  |apply in_list_cons;apply H;assumption
+  ]
+qed.*)
+
+naxiom in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
+\forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
+(*intros 3.
+elim l
+  [right.apply H
+  |simplify in H1.inversion H1;intros; destruct;
+    [left.apply in_list_head
+    | elim (H l2)
+      [left.apply in_list_cons. assumption
+      |right.assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.*)
+
+nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
+ match l with
+  [ nil ⇒ false
+  | (cons a l') ⇒
+    match eq x a with
+     [ true ⇒ true
+     | false ⇒ mem A eq x l'
+     ]
+  ].
+  
+naxiom mem_true_to_in_list :
+  \forall A,equ.
+  (\forall x,y.equ x y = true \to x = y) \to
+  \forall x,l.mem A equ x l = true \to in_list A x l.
+(* intros 5.elim l
+  [simplify in H1;destruct H1
+  |simplify in H2;apply (bool_elim ? (equ x a))
+     [intro;rewrite > (H ? ? H3);apply in_list_head
+     |intro;rewrite > H3 in H2;simplify in H2;
+      apply in_list_cons;apply H1;assumption]]
+qed.*)
+
+naxiom in_list_to_mem_true :
+  \forall A,equ.
+  (\forall x.equ x x = true) \to
+  \forall x,l.in_list A x l \to mem A equ x l = true.
+(*intros 5.elim l
+  [elim (not_in_list_nil ? ? H1)
+  |elim H2
+    [simplify;rewrite > H;reflexivity
+    |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
+qed.*)
+
+naxiom in_list_filter_to_p_true : \forall A,l,x,p.
+in_list A x (filter A l p) \to p x = true.
+(* intros 4;elim l
+  [simplify in H;elim (not_in_list_nil ? ? H)
+  |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
+   simplify in H1
+     [elim (in_list_cons_case ? ? ? ? H1)
+        [rewrite > H3;assumption
+        |apply (H H3)]
+     |apply (H H1)]]
+qed.*)
+
+naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
+(*intros 4;elim l
+  [simplify in H;elim (not_in_list_nil ? ? H)
+  |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
+   simplify in H1
+     [elim (in_list_cons_case ? ? ? ? H1)
+        [rewrite > H3;apply in_list_head
+        |apply in_list_cons;apply H;assumption]
+     |apply in_list_cons;apply H;assumption]]
+qed.*)
+
+naxiom in_list_filter_r : \forall A,l,p,x.
+              in_list A x l \to p x = true \to in_list A x (filter A l p).
+(* intros 4;elim l
+  [elim (not_in_list_nil ? ? H)
+  |elim (in_list_cons_case ? ? ? ? H1)
+     [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
+     |simplify;apply (bool_elim ? (p a));intro;simplify;
+        [apply in_list_cons;apply H;assumption
+        |apply H;assumption]]]
+qed.*)
+
+naxiom incl_A_A: ∀T,A.incl T A A.
+(*intros.unfold incl.intros.assumption.
+qed.*)
+
+naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
+(*unfold incl; intros;autobatch.
+qed.*)
+
+naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
+(*unfold incl; intros;autobatch.
+qed.*)
+
+naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
+(*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
+qed.*)
+
diff --git a/helm/software/matita/nlibrary/datatypes/pairs.ma b/helm/software/matita/nlibrary/datatypes/pairs.ma
index dfff0c3f8..2165accbb 100644
--- a/helm/software/matita/nlibrary/datatypes/pairs.ma
+++ b/helm/software/matita/nlibrary/datatypes/pairs.ma
@@ -17,4 +17,15 @@ include "logic/pts.ma".
 nrecord pair (A,B: Type[0]) : Type[0] ≝
  { fst: A;
    snd: B
- }.
\ No newline at end of file
+ }.
+
+interpretation "Pair construction" 'pair x y = (mk_pair ? ? x y).
+
+interpretation "Product" 'product x y = (pair x y).
+
+interpretation "pair pi1" 'pi1 = (fst ? ?).
+interpretation "pair pi2" 'pi2 = (snd ? ?).
+interpretation "pair pi1" 'pi1a x = (fst ? ? x).
+interpretation "pair pi2" 'pi2a x = (snd ? ? x).
+interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
+interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
diff --git a/helm/software/matita/nlibrary/datatypes/sums.ma b/helm/software/matita/nlibrary/datatypes/sums.ma
new file mode 100644
index 000000000..c5a73b4b5
--- /dev/null
+++ b/helm/software/matita/nlibrary/datatypes/sums.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___	                                                            *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "datatypes/pairs.ma".
+
+ninductive void : Type[0] ≝.
+
+ninductive unit : Type[0] ≝ something: unit.
+
+ninductive Sum (A,B:Type[0]) : Type[0] ≝
+| inl : A → Sum A B
+| inr : B → Sum A B.
+
+interpretation "Disjoint union" 'plus A B = (Sum A B).
+
+ninductive option (A:Type[0]) : Type[0] ≝
+ | None : option A
+ | Some : A → option A.
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index 8ae1bcde4..f1a679c7d 100644
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -125,4 +125,94 @@ ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
   | napply refl
   | #x; #y; #H; nrewrite < H; napply refl
   | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]
-nqed.
\ No newline at end of file
+nqed.
+
+naxiom T1 : Type[0].
+naxiom T2 : T1 → Type[0].
+naxiom t1 : T1.
+naxiom t2 : ∀x:T1. T2 x.
+
+ninductive I2 : ∀r1:T1.T2 r1 → Type[0] ≝ 
+| i2c1 : ∀x1:T1.∀x2:T2 x1. I2 x1 x2
+| i2c2 : I2 t1 (t2 t1).
+
+(* nlemma i2d : ∀a,b.∀x,y:I2 a b.
+             ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
+             ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.
+             Type[2].
+#a;#b;#x;#y;
+napply (
+match x return (λr1,r2,r.
+                 ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b.
+                 ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with 
+  [ i2c1 x1 x2 ⇒ ?
+  | i2c2 ⇒ ?] 
+)
+[napply (match y return (λr1,r2,r.
+                     ∀e1: x1 = r1. ∀e2: R1 T1 x1 (λz,p. T2 z) x2 r1 e1 = r2.
+                     ∀e : R2 T1 x1 (λz,p.T2 z) x2 (λz1,p1,z2,p2. I2 z1 z2) (i2c1 x1 x2) r1 e1 r2 e2 = r. Type[2]) with
+    [ i2c1 y1 y2 ⇒ ?
+    | i2c2 ⇒ ? ])
+ [#e1; #e2; #e;
+  napply (∀P:Type[1].
+                     (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
+                      ∀f: R2 T1 x1 (λz,p.T2 z) x2
+                          (λz1,p1,z2,p2.eq ? 
+                              (i2c1 (R1 ??? z1 ? (R1 ?? (λm,n.m = y1) f1 ? p1)) ?)
+                               (*       (R2 ???? (λm1,n1,m2,n2.R1 ?? (λm,n.T2 m) ? ? f1 = y2) f2 ? 
+                                       p1 ? p2)))*)
+(*                            (R2 ???? (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2) 
+                                ? (R1 ?? (λw,q.w = y1) e1 z1 p1) 
+                                ? (R2 ????
+                                      (λw1,q1,w2,q2.R1 ?? (λm,n.T2 m) w2 ? q1 = y2) 
+                                      e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
+  *)                          (i2c1 y1 y2)) 
+                          ? y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P) 
+                   → P);
+  napply (∀P:Type[1].
+                     (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2. 
+                      ∀f: R2 T1 x1 (λz,p.T2 z) x2
+                          (λz1,p1,z2,p2.eq (I2 y1 y2) 
+                            (R2 T1 z1 (λw,q.T2 w) z2 (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2) 
+                                y1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) 
+                                y2 (R2 T1 x1 (λw,q.w = y1) e1 
+                                             (λw1,q1,w2,q2.R1 ??? w2 w1 q1 = y2) e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
+                            (i2c1 y1 y2)) 
+                          e y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P) 
+                   → P);
+
+
+ndefinition i2d : ∀a,b.∀x,y:I2 a b.
+                  ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
+                  ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.Type[2] ≝
+λa,b,x,y. 
+match x return (λr1,r2,r.
+                 ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b.
+                 ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with 
+  [ i2c1 x1 x2 ⇒ 
+    match y return (λr1,r2,r.
+                     ∀e1: x1 = r1. ∀e2: R1 T1 x1 (λz,p. T2 z) x2 r1 e1 = r2.
+                     ∀e : R2 T1 x1 (λz,p.T2 z) x2 (λz1,p1,z2,p2. I2 z1 z2) (i2c1 x1 x2) r1 e1 r2 e2 = r. Type[2]) with
+    [ i2c1 y1 y2 ⇒ λe1,e2,e.∀P:Type[1].
+                     (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2. 
+                      ∀f: R2 T1 x1 (λz,p.T2 z) x2
+                          (λz1,p1,z2,p2.eq (I2 y1 y2) 
+                            (R2 T1 z1 (λw,q.T2 w) z2 (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2) 
+                                y1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) 
+                                y2 (R2 T1 x1 (λw,q.w = y1) e1 
+                                             (λw1,q1,w2,q2.R1 ??? w2 w1 q1 = y2) e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
+                            (i2c1 y1 y2)) 
+                          e y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P) 
+                   → P
+    | i2c2 ⇒ λe1,e2,e.∀P:Type[1].P ]
+  | i2c2 ⇒ 
+    match y return (λr1,r2,r.
+                     ∀e1: x1 = r1. ∀e2: R1 ?? (λz,p. T2 z) x2 ? e1 = r2.
+                     ∀e : R2 ???? (λz1,p1,z2,p2. I2 z1 z2) i2c2 ? e1 ? e2 = r. Type[2]) with
+    [ i2c1 _ _ ⇒ λe1,e2,e.∀P:Type[1].P
+    | i2c2 ⇒ λe1,e2,e.∀P:Type[1].
+               (∀f: R2 ???? 
+                    (λz1,p1,z2,p2.eq ? i2c2 i2c2) 
+                    e ? e1 ? e2 = refl ? i2c2.P) → P ] ].
+
+*)
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 780dc2b4c..d4a13507c 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -52,8 +52,8 @@ ndefinition seteq: ∀A. equivalence_relation1 (Ω^A).
  #A; @
   [ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S)
   | /2/
-  | #S; #S'; *; /2/
-  | #S; #T; #U; *; #H1; #H2; *; /3/]
+  | #S; #S'; *; /3/
+  | #S; #T; #U; *; #H1; #H2; *; /4/]
 nqed.
 
 include "sets/setoids1.ma".
@@ -140,7 +140,7 @@ unification hint 0 ≔  A:setoid, x, S;
 nlemma subseteq_is_morph: ∀A. unary_morphism1 (ext_powerclass_setoid A)
  (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP).
  #A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S'));
- #a; #a'; #b; #b'; *; #H1; #H2; *; /4/.
+ #a; #a'; #b; #b'; *; #H1; #H2; *; /5/.
 nqed.
 
 unification hint 0 ≔ A,a,a'