X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fnlibrary%2Fproperties%2Frelations2.ma;fp=matitaB%2Fmatita%2Fnlibrary%2Fproperties%2Frelations2.ma;h=155dde75b274e488ef24cf31bc02844f852610bc;hb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;hp=67d09e9383c91f00c081479404456ea19096da25;hpb=98f0fac6d03367be776303e7ba353b75878aaa40;p=helm.git

diff --git a/matitaB/matita/nlibrary/properties/relations2.ma b/matitaB/matita/nlibrary/properties/relations2.ma
index 67d09e938..155dde75b 100644
--- a/matitaB/matita/nlibrary/properties/relations2.ma
+++ b/matitaB/matita/nlibrary/properties/relations2.ma
@@ -14,13 +14,13 @@
 
 include "logic/pts.ma".
 
-ndefinition reflexive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x.P x x.
-ndefinition symmetric2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x,y.P x y → P y x.
-ndefinition transitive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀z,x,y. P x z → P z y → P x y.
+definition reflexive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x.P x x.
+definition symmetric2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x,y.P x y → P y x.
+definition transitive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀z,x,y. P x z → P z y → P x y.
 
-nrecord equivalence_relation2 (A:Type[2]) : Type[3] ≝
+record equivalence_relation2 (A:Type[2]) : Type[3] ≝
  { eq_rel2:2> A → A → CProp[2];
-   refl2: reflexive2 ? eq_rel2;
-   sym2: symmetric2 ? eq_rel2;
-   trans2: transitive2 ? eq_rel2
+   refl2: <A href="cic:/matita/ng/properties/relations2/reflexive2.def(1)">reflexive2</A> ? eq_rel2;
+   sym2: <A href="cic:/matita/ng/properties/relations2/symmetric2.def(1)">symmetric2</A> ? eq_rel2;
+   trans2: <A href="cic:/matita/ng/properties/relations2/transitive2.def(1)">transitive2</A> ? eq_rel2
  }.