Commented a few lemmas (copies).

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

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