X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fnlibrary%2Fproperties%2Frelations2.ma;h=155dde75b274e488ef24cf31bc02844f852610bc;hb=100184e7920cc3c70b50b694a17fa40ecde45e77;hp=67d09e9383c91f00c081479404456ea19096da25;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;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: reflexive2 ? eq_rel2;
+ sym2: symmetric2 ? eq_rel2;
+ trans2: transitive2 ? eq_rel2
}.