From d3d67acad6b7a946036c38bd2096609a29fef773 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 17 Mar 2010 11:47:03 +0000 Subject: [PATCH 1/1] Nuova definizione della negazione. --- helm/software/matita/nlibrary/basics/eq.ma | 9 +++++++++ 1 file changed, 9 insertions(+) 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. -- 2.39.2