From 11a6c88f3e717b019be2eae71711c70473b5467a Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Tue, 21 Jul 2009 22:37:37 +0000
Subject: [PATCH]  freescale porting, work in progress

---
 .../contribs/ng_assembly/freescale/bool.ma    |  12 --
 .../ng_assembly/freescale/bool_lemmas.ma      |   8 +-
 .../ng_assembly/freescale/exadecim.ma         |  32 +-----
 .../contribs/ng_assembly/freescale/nat.ma     |   9 --
 .../contribs/ng_assembly/freescale/prod.ma    | 108 ------------------
 .../contribs/ng_assembly/freescale/theory.ma  |  67 +----------
 6 files changed, 11 insertions(+), 225 deletions(-)

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool.ma
index 7f7dba743..e7ea4dcfa 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/bool.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool.ma
@@ -30,18 +30,6 @@ ninductive bool : Type ≝
   true : bool
 | false : bool.
 
-ndefinition bool_ind : ΠP:bool → Prop.P true → P false → Πb:bool.P b ≝
-λP:bool → Prop.λp:P true.λp1:P false.λb:bool.
- match b with [ true ⇒ p | false ⇒ p1 ].
-
-ndefinition bool_rec : ΠP:bool → Set.P true → P false → Πb:bool.P b ≝
-λP:bool → Set.λp:P true.λp1:P false.λb:bool.
- match b with [ true ⇒ p | false ⇒ p1 ].
-
-ndefinition bool_rect : ΠP:bool → Type.P true → P false → Πb:bool.P b ≝
-λP:bool → Type.λp:P true.λp1:P false.λb:bool.
- match b with [ true ⇒ p | false ⇒ p1 ].
-
 (* operatori booleani *)
 
 ndefinition eq_bool ≝
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
index bc146e793..7d6006862 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
@@ -40,12 +40,14 @@ ndefinition bool_destruct : bool_destruct_aux.
  nelim b2;
  nnormalize;
  #H;
- ##[ ##2: napply (False_ind ??);
+ ##[ ##2: napply (False_ind (λx.P) ?);
+          (* perche' non napply (False_ind ??); !!! *)
           nchange with (match true with [ true ⇒ False | false ⇒ True]);
           nrewrite > H;
           nnormalize;
           napply I
- ##| ##3: napply (False_ind ??);
+ ##| ##3: napply (False_ind (λx.P) ?);
+          (* perche' non napply (False_ind ??); !!! *)
           nchange with (match true with [ true ⇒ False | false ⇒ True]);
           nrewrite < H;
           nnormalize;
@@ -104,7 +106,7 @@ nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
  napply (refl_eq ??).
 nqed.
 
-nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
+nlemma associative_xorbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
  #b1; #b2; #b3;
  nelim b1;
  nelim b2;
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma b/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
index 44baf0f03..f6cb78d33 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
@@ -28,6 +28,8 @@ include "freescale/nat.ma".
 (* ESADECIMALI *)
 (* *********** *)
 
+(* non riesce a terminare l'esecuzione !!! *)
+
 ninductive exadecim : Type ≝
   x0: exadecim
 | x1: exadecim
@@ -46,36 +48,6 @@ ninductive exadecim : Type ≝
 | xE: exadecim
 | xF: exadecim.
 
-ndefinition exadecim_ind :
- ΠP:exadecim → Prop.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
-                    P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
-λP:exadecim → Prop.
-λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
-λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
- match e with
-  [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
-  | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].                                     
-
-ndefinition exadecim_rec :
- ΠP:exadecim → Set.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
-                    P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
-λP:exadecim → Set.
-λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
-λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
- match e with
-  [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
-  | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].                                        
-
-ndefinition exadecim_rect :
- ΠP:exadecim → Type.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
-                    P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
-λP:exadecim → Type.
-λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
-λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
- match e with
-  [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
-  | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].   
-
 (* operatore = *)
 ndefinition eq_ex ≝
 λe1,e2:exadecim.
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/nat.ma b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
index aacc7b1dd..4753b4cac 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
@@ -37,15 +37,6 @@ default "natural numbers" cic:/matita/freescale/nat/nat.ind.
 
 alias num (instance 0) = "natural number".
 
-nlet rec nat_ind (P:nat → Prop) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
- match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_ind P p f n1) ].
-
-nlet rec nat_rec (P:nat → Set) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
- match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rec P p f n1) ].
-
-nlet rec nat_rect (P:nat → Type) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
- match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rect P p f n1) ].
-
 nlet rec eq_nat (n1,n2:nat) on n1 ≝
  match n1 with
   [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
index 48d054d3a..e382b0dd1 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
@@ -29,33 +29,6 @@ include "freescale/bool.ma".
 ninductive ProdT (T1:Type) (T2:Type) : Type ≝
  pair : T1 → T2 → ProdT T1 T2.
 
-ndefinition ProdT_ind
- : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Prop.
-   (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
-   Πp:ProdT T1 T2.P p ≝
-λT1,T2:Type.λP:ProdT T1 T2 → Prop.
-λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
-λp:ProdT T1 T2.
- match p with [ pair t t1 ⇒ f t t1 ].
-
-ndefinition ProdT_rec
- : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Set.
-   (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
-   Πp:ProdT T1 T2.P p ≝
-λT1,T2:Type.λP:ProdT T1 T2 → Set.
-λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
-λp:ProdT T1 T2.
- match p with [ pair t t1 ⇒ f t t1 ].
-
-ndefinition ProdT_rect
- : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Type.
-   (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
-   Πp:ProdT T1 T2.P p ≝
-λT1,T2:Type.λP:ProdT T1 T2 → Type.
-λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
-λp:ProdT T1 T2.
- match p with [ pair t t1 ⇒ f t t1 ].
-
 ndefinition fst ≝
 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  x _ ⇒ x ].
 
@@ -72,33 +45,6 @@ ndefinition eq_pair ≝
 ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
 triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
 
-ndefinition Prod3T_ind
- : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Prop.
-   (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
-   Πp:Prod3T T1 T2 T3.P p ≝
-λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Prop.
-λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
-λp:Prod3T T1 T2 T3.
- match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
-
-ndefinition Prod3T_rec
- : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Set.
-   (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
-   Πp:Prod3T T1 T2 T3.P p ≝
-λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Set.
-λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
-λp:Prod3T T1 T2 T3.
- match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
-
-ndefinition Prod3T_rect
- : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Type.
-   (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
-   Πp:Prod3T T1 T2 T3.P p ≝
-λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Type.
-λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
-λp:Prod3T T1 T2 T3.
- match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
-
 ndefinition fst3T ≝
 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple x _ _ ⇒ x ].
 
@@ -118,33 +64,6 @@ ndefinition eq_triple ≝
 ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
 quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
 
-ndefinition Prod4T_ind
- : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Prop.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
-   Πp:Prod4T T1 T2 T3 T4.P p ≝
-λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Prop.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
-λp:Prod4T T1 T2 T3 T4.
- match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
-
-ndefinition Prod4T_rec
- : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Set.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
-   Πp:Prod4T T1 T2 T3 T4.P p ≝
-λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Set.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
-λp:Prod4T T1 T2 T3 T4.
- match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
-
-ndefinition Prod4T_rect
- : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Type.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
-   Πp:Prod4T T1 T2 T3 T4.P p ≝
-λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Type.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
-λp:Prod4T T1 T2 T3 T4.
- match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
-
 ndefinition fst4T ≝
 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple x _ _ _ ⇒ x ].
 
@@ -167,33 +86,6 @@ ndefinition eq_quadruple ≝
 ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
 quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
 
-ndefinition Prod5T_ind
- : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Prop.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
-   Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
-λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Prop.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
-λp:Prod5T T1 T2 T3 T4 T5.
- match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-
-ndefinition Prod5T_rec
- : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Set.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
-   Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
-λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Set.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
-λp:Prod5T T1 T2 T3 T4 T5.
- match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-
-ndefinition Prod5T_rect
- : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Type.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
-   Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
-λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Type.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
-λp:Prod5T T1 T2 T3 T4 T5.
- match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-
 ndefinition fst5T ≝
 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple x _ _ _ _ ⇒ x ].
 
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
index 3e108e7be..5a7f658ec 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
@@ -31,32 +31,8 @@ include "freescale/pts.ma".
 ninductive True: Prop ≝
  I : True.
 
-(*ndefinition True_ind_xx : ΠP:Prop.P → True → P ≝
-λP:Prop.λp:P.λH:True.
- match H with [ I ⇒ p ].
-
-ndefinition True_rec_xx : ΠP:Set.P → True → P ≝
-λP:Set.λp:P.λH:True.
- match H with [ I ⇒ p ].
-
-ndefinition True_rect_xx : ΠP:Type.P → True → P ≝
-λP:Type.λp:P.λH:True.
- match H with [ I ⇒ p ].*)
-
 ninductive False: Prop ≝.
 
-(*ndefinition False_ind_xx : ΠP:Prop.False → P ≝
-λP:Prop.λH:False.
- match H in False return λH1:False.P with [].
-
-ndefinition False_rec_xx : ΠP:Set.False → P ≝
-λP:Set.λH:False.
- match H in False return λH1:False.P with [].
-
-ndefinition False_rect_xx : ΠP:Type.False → P ≝
-λP:Type.λH:False.
- match H in False return λH1:False.P with [].*)
-
 ndefinition Not: Prop → Prop ≝
 λA.(A → False).
 
@@ -79,18 +55,6 @@ nqed.
 ninductive And (A,B:Prop) : Prop ≝
  conj : A → B → (And A B).
 
-(*ndefinition And_ind_xx : ΠA,B:Prop.ΠP:Prop.(A → B → P) → And A B → P ≝
-λA,B:Prop.λP:Prop.λf:A → B → P.λH:And A B.
- match H with [conj H1 H2 ⇒ f H1 H2 ].
-
-ndefinition And_rec_xx : ΠA,B:Prop.ΠP:Set.(A → B → P) → And A B → P ≝
-λA,B:Prop.λP:Set.λf:A → B → P.λH:And A B.
- match H with [conj H1 H2 ⇒ f H1 H2 ].
-
-ndefinition And_rect_xx : ΠA,B:Prop.ΠP:Type.(A → B → P) → And A B → P ≝
-λA,B:Prop.λP:Type.λf:A → B → P.λH:And A B.
- match H with [conj H1 H2 ⇒ f H1 H2 ].*)
-
 interpretation "logical and" 'and x y = (And x y).
 
 nlemma proj1: ∀A,B:Prop.A ∧ B → A.
@@ -111,10 +75,6 @@ ninductive Or (A,B:Prop) : Prop ≝
   or_introl : A → (Or A B)
 | or_intror : B → (Or A B).
 
-(*ndefinition Or_ind_xx : ΠA,B:Prop.ΠP:Prop.(A → P) → (B → P) → Or A B → P ≝
-λA,B:Prop.λP:Prop.λf1:A → P.λf2:B → P.λH:Or A B.
- match H with [ or_introl H1 ⇒ f1 H1 | or_intror H1 ⇒ f2 H1 ].*)
-
 interpretation "logical or" 'or x y = (Or x y).
 
 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
@@ -122,19 +82,11 @@ ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
  ex_intro: ∀x:A.Q x → ex A Q.
 
-(*ndefinition ex_ind_xx : ΠA:Type.ΠQ:A → Prop.ΠP:Prop.(Πa:A.Q a → P) → ex A Q → P ≝
-λA:Type.λQ:A → Prop.λP:Prop.λf:(Πa:A.Q a → P).λH:ex A Q.
- match H with [ ex_intro H1 H2 ⇒ f H1 H2 ].*)
-
 interpretation "exists" 'exists x = (ex ? x).
 
 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 
-(*ndefinition ex2_ind_xx : ΠA:Type.ΠQ,R:A → Prop.ΠP:Prop.(Πa:A.Q a → R a → P) → ex2 A Q R → P ≝
-λA:Type.λQ,R:A → Prop.λP:Prop.λf:(Πa:A.Q a → R a → P).λH:ex2 A Q R.
- match H with [ ex_intro2 H1 H2 H3 ⇒ f H1 H2 H3 ].*)
-
 ndefinition iff ≝
 λA,B.(A -> B) ∧ (B -> A).
 
@@ -169,18 +121,6 @@ ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 ninductive eq (A:Type) (x:A) : A → Prop ≝
  refl_eq : eq A x x.
 
-(*ndefinition eq_ind_xx : ΠA:Type.Πx:A.ΠP:A → Prop.P x → Πa:A.eq A x a → P a ≝
-λA:Type.λx:A.λP:A → Prop.λp:P x.λa:A.λH:eq A x a.
- match H with [refl_eq ⇒ p ].
-
-ndefinition eq_rec_xx : ΠA:Type.Πx:A.ΠP:A → Set.P x → Πa:A.eq A x a → P a ≝
-λA:Type.λx:A.λP:A → Set.λp:P x.λa:A.λH:eq A x a.
- match H with [refl_eq ⇒ p ].
-
-ndefinition eq_rect_xx : ΠA:Type.Πx:A.ΠP:A → Type.P x → Πa:A.eq A x a → P a ≝
-λA:Type.λx:A.λP:A → Type.λp:P x.λa:A.λH:eq A x a.
- match H with [refl_eq ⇒ p ].*)
-
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
@@ -195,9 +135,8 @@ nqed.
 
 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  #A; #x; #P; #H; #y; #H1;
- nletin H2 ≝ (symmetric_eq ??? H1);
- nrewrite < H2;
- nassumption.
+ nrewrite < (symmetric_eq ??? H1);
+ napply H.
 nqed.
 
 ndefinition relationT : Type → Type → Type ≝
@@ -270,6 +209,7 @@ nqed.
 
 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
  #T; #l;
+ (* perche' non nelim l; !!! *)
  napply (list_ind T ??? l);
  nnormalize;
  ##[ ##1: napply (refl_eq ??)
@@ -281,6 +221,7 @@ nqed.
 
 nlemma associative_list : ∀T.associative (list T) (append T).
  #T; #x; #y; #z;
+ (* perche' non nelim x; !!! *)
  napply (list_ind T ??? x);
  nnormalize;
  ##[ ##1: napply (refl_eq ??)
-- 
2.39.2