X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Ftheory.ma;h=7f5f9003658d6d621d2b8240357f4ada4565a1a0;hb=9dc61a4f11210bccf34f63f48968afca4261c1b4;hp=c4bd19f167a1974ff29e08707c916e27da28a92b;hpb=fc1e871dde0f9f4cfde6f4a4fda8d18022584e65;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index c4bd19f16..7f5f90036 100644
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -45,7 +45,7 @@ nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  nelim (H1 H);
 nqed.
 
-nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
+nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
  #A; #B; #H;
  nnormalize;
  #H1; #H2;
@@ -304,6 +304,14 @@ nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  napply H.
 nqed.
 
+nlemma symmetric_neq : ∀T.∀x,y:T.x ≠ y → y ≠ x.
+ #T; #x; #y;
+ nnormalize;
+ #H; #H1;
+ nrewrite > H1 in H:(%); #H;
+ napply (H (refl_eq …)).
+nqed.
+
 ndefinition relationT : Type → Type → Type ≝
 λA,T:Type.A → A → T.