Commented a few lemmas (copies).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/matita/nlibrary/basics/eq.ma b/helm/software/matita/nlibrary/basics/eq.ma
index 61047a474ca5ca1516d56c982de7d09e2a3c3de2..56a73337875ff61096493a49214604a85f552f74 100644 (file)
--- a/helm/software/matita/nlibrary/basics/eq.ma
+++ b/helm/software/matita/nlibrary/basics/eq.ma
@@ -16,11 +16,13 @@ include "basics/relations.ma".
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 
+(* this is refl 
 ntheorem reflexive_eq : ∀A:Type. reflexive A (eq A).
-//; nqed.
-  
+//; nqed. *)
+
+(* this is sym_eq 
 ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
-//; nqed.
+//; nqed. *)
 
 ntheorem transitive_eq : ∀A:Type. transitive A (eq A).
 #A; #x; #y; #z; #H1; #H2; nrewrite > H1; //; nqed.
@@ -46,7 +48,8 @@ theorem eq_f': \forall  A,B:Type.\forall f:A\to B.
 intros.elim H.apply refl_eq.
 qed. *)
 
+(* deleterio per auto
 ntheorem eq_f2: ∀A,B,C:Type.∀f:A→B→C.
 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
 #A; #B; #C; #f; #x1; #x2; #y1; #y2; #E1; #E2; nrewrite > E1; nrewrite > E2;//.
-nqed.
\ No newline at end of file
+nqed. *)
\ No newline at end of file

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.