X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fbasics%2Feq.ma;h=4a29e2843a7103873530343383781682866abb0d;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=73abc9f09c2098b14ff5982f7deef0aedda47ccd;hpb=34311f3f810eb893b865d1893eae1cf62cd490b4;p=helm.git

diff --git a/helm/software/matita/nlibrary/basics/eq.ma b/helm/software/matita/nlibrary/basics/eq.ma
index 73abc9f09..4a29e2843 100644
--- a/helm/software/matita/nlibrary/basics/eq.ma
+++ b/helm/software/matita/nlibrary/basics/eq.ma
@@ -16,17 +16,28 @@ 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.
 
+(*
 ntheorem symmetric_not_eq: ∀A:Type. symmetric A (λx,y.x ≠ y).
+/3/; nqed.
+*)
+
+ntheorem symmetric_not_eq: ∀A:Type. ∀x,y:A. x ≠ y → y ≠ x.
+/3/; nqed.
+
+(*
 #A; #x; #y; #H; #K; napply H; napply symmetric_eq; //; nqed.
+*)
 
 ntheorem eq_f: ∀A,B:Type.∀f:A→B.∀x,y:A. x=y → f x = f y.
 #A; #B; #f; #x; #y; #H; nrewrite > H; //; nqed.
@@ -37,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