Release 0.5.9.

[helm.git] / helm / software / matita / contribs / ng_assembly / common / list_lemmas.ma

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 3be3a0a8997cd20a2534cc92184312e6cfb5f928..90461cfca9050dd455393cdc2bcfd0c957258695 100644 (file)
--- 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              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -42,7 +42,6 @@ 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 ]);
@@ -51,7 +50,6 @@ 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 ]);
@@ -123,7 +121,6 @@ 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 ]);
@@ -132,7 +129,6 @@ 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 ]);