Commented a few lemmas (copies).

[helm.git] / helm / software / matita / nlibrary / basics / list.ma

diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma
index d30ed7dfc2a4833f503224f940b7d37c2a866392..3d41b946c73a7929a227c529ab313f7d3a273c8e 100644 (file)
--- a/helm/software/matita/nlibrary/basics/list.ma
+++ b/helm/software/matita/nlibrary/basics/list.ma
@@ -73,10 +73,11 @@ ntheorem associative_append:
  ∀A:Type.associative (list A) (append A).
 #A; #l1; #l2; #l3; nelim l1; nnormalize; //; nqed.
 
+(* deleterio per auto 
 ntheorem cons_append_commute:
   ∀A:Type.∀l1,l2:list A.∀a:A.
     a :: (l1 @ l2) = (a :: l1) @ l2.
-//; nqed.
+//; nqed. *)
 
 ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
 #A; #a; #l; #l1; napply symmetric_eq.