freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / common / theory.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index c4bd19f167a1974ff29e08707c916e27da28a92b..7f5f9003658d6d621d2b8240357f4ada4565a1a0 100644 (file)
--- 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.