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=a79bf6edc13daaea8135ca71fdc92e02e229f030;hp=90461cfca9050dd455393cdc2bcfd0c957258695;hpb=38fccc2b774e493a94eedef76342b56079c0e694;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 90461cfca..3be3a0a89 100644
--- a/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   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 ]);