X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Flist_lemmas.ma;h=3be3a0a8997cd20a2534cc92184312e6cfb5f928;hb=603f2f6b596d8632b9bd53c73ae0b9c3575231e0;hp=51654011ee79a8c4060044cb1d08d46b915c978f;hpb=db235934efa41a0f38e79747f6db4f468367410b;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma
index 51654011e..3be3a0a89 100644
--- a/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -42,6 +42,7 @@ nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x
  napply refl_eq.
 nqed.
 
+(* !!! da togliere *)
 nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
  #T; #x; #y; #H;
  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
@@ -50,6 +51,7 @@ nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → F
  napply I.
 nqed.
 
+(* !!! da togliere *)
 nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
  #T; #x; #y; #H;
  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
@@ -121,6 +123,7 @@ nlemma nelist_destruct_cons_cons_2 : ∀T.∀x1,x2:T.∀y1,y2:ne_list T.ne_cons
  napply refl_eq.
 nqed.
 
+(* !!! da togliere *)
 nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y1 = ne_nil T x2 → False.
  #T; #x1; #x2; #y1; #H;
  nchange with (match ne_cons T x1 y1 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);
@@ -129,6 +132,7 @@ nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y
  napply I.
 nqed.
 
+(* !!! da togliere *)
 nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False.
  #T; #x1; #x2; #y2; #H;
  nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]);