From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 17 Mar 2010 11:47:03 +0000 (+0000)
Subject: Nuova definizione della negazione.
X-Git-Tag: make_still_working~3005
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d3d67acad6b7a946036c38bd2096609a29fef773;p=helm.git

Nuova definizione della negazione.
---

diff --git a/helm/software/matita/nlibrary/basics/eq.ma b/helm/software/matita/nlibrary/basics/eq.ma
index 73abc9f09..61047a474 100644
--- a/helm/software/matita/nlibrary/basics/eq.ma
+++ b/helm/software/matita/nlibrary/basics/eq.ma
@@ -25,8 +25,17 @@ ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
 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.