X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Ftheory.ma;h=65800d2e5011e2b0a38769bd4e29ed2aafc4de3a;hb=64bdbee95e40a5be3bb6c5c2866869103730a4d0;hp=ceda6dccac7680d1b491918fa64f8b1e28df4da9;hpb=47f4d2af2a592e2e6c0e0ea5f90ffae2fbf6391a;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
index ceda6dcca..65800d2e5 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
@@ -64,14 +64,14 @@ ndefinition Not: Prop → Prop ≝
 
 interpretation "logical not" 'not x = (Not x).
 
-ntheorem absurd : ∀A,C:Prop.A → ¬A → C.
+nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  #A; #C; #H;
  nnormalize;
  #H1;
  nelim (H1 H).
 nqed.
 
-ntheorem 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;
@@ -95,14 +95,14 @@ ndefinition And_rect : ΠA,B:Prop.ΠP:Type.(A → B → P) → And A B → P ≝
 
 interpretation "logical and" 'and x y = (And x y).
 
-ntheorem proj1: ∀A,B:Prop.A ∧ B → A.
+nlemma proj1: ∀A,B:Prop.A ∧ B → A.
  #A; #B; #H;
  napply (And_ind A B ?? H);
  #H1; #H2;
  napply H1.
 nqed.
 
-ntheorem proj2: ∀A,B:Prop.A ∧ B → B.
+nlemma proj2: ∀A,B:Prop.A ∧ B → B.
  #A; #B; #H;
  napply (And_ind A B ?? H);
  #H1; #H2;
@@ -183,7 +183,7 @@ interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 
-ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
+nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  #A;
  nnormalize;
  #x; #y; #H;
@@ -191,9 +191,15 @@ ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
  napply (refl_eq ??).
 nqed.
 
-ntheorem eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  #A; #x; #P; #H; #y; #H1;
  napply (eq_ind ? x ? H y ?);
  nrewrite < H1;
  napply (refl_eq ??).
 nqed.
+
+ndefinition relationT : Type → Type → Type ≝
+λA,T:Type.A → A → T.
+
+ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
+λA,T.λR.∀x,y:A.R x y = R y x.