X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fnlibrary%2Fproperties%2Frelations1.ma;h=535a11984524b5978c6fc4092129b3befaada052;hb=100184e7920cc3c70b50b694a17fa40ecde45e77;hp=86a6f15b707b61318ab122c766db38c6fef4bc85;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git
diff --git a/matitaB/matita/nlibrary/properties/relations1.ma b/matitaB/matita/nlibrary/properties/relations1.ma
index 86a6f15b7..535a11984 100644
--- a/matitaB/matita/nlibrary/properties/relations1.ma
+++ b/matitaB/matita/nlibrary/properties/relations1.ma
@@ -14,13 +14,13 @@
include "logic/pts.ma".
-ndefinition reflexive1 â λT:Type[1].λP:T â T â CProp[1]. âx.P x x.
-ndefinition symmetric1 â λT:Type[1].λP:T â T â CProp[1]. âx,y.P x y â P y x.
-ndefinition transitive1 â λT:Type[1].λP:T â T â CProp[1]. âz,x,y. P x z â P z y â P x y.
+definition reflexive1 â λT:Type[1].λP:T â T â CProp[1]. âx.P x x.
+definition symmetric1 â λT:Type[1].λP:T â T â CProp[1]. âx,y.P x y â P y x.
+definition transitive1 â λT:Type[1].λP:T â T â CProp[1]. âz,x,y. P x z â P z y â P x y.
-nrecord equivalence_relation1 (A:Type[1]) : Type[2] â
+record equivalence_relation1 (A:Type[1]) : Type[2] â
{ eq_rel1:2> A â A â CProp[1];
- refl1: reflexive1 ? eq_rel1;
- sym1: symmetric1 ? eq_rel1;
- trans1: transitive1 ? eq_rel1
+ refl1: reflexive1 ? eq_rel1;
+ sym1: symmetric1 ? eq_rel1;
+ trans1: transitive1 ? eq_rel1
}.