X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fnlibrary%2Fproperties%2Frelations.ma;h=334c67842f8762ecee087a7dd103f8ba0e886345;hb=100184e7920cc3c70b50b694a17fa40ecde45e77;hp=1df2e205a5d097a2680ad0864d92145ada7c9906;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git
diff --git a/matitaB/matita/nlibrary/properties/relations.ma b/matitaB/matita/nlibrary/properties/relations.ma
index 1df2e205a..334c67842 100644
--- a/matitaB/matita/nlibrary/properties/relations.ma
+++ b/matitaB/matita/nlibrary/properties/relations.ma
@@ -20,7 +20,7 @@ definition transitive â λT:Type[0].λP:T â T â CProp[0]. âz,x,y. P x z
record equivalence_relation (A:Type[0]) : Type[1] â
{ eq_rel:2> A â A â CProp[0];
- refl: reflexive ? eq_rel;
- sym: symmetric ? eq_rel;
- trans: transitive ? eq_rel
+ refl: reflexive ? eq_rel;
+ sym: symmetric ? eq_rel;
+ trans: transitive ? eq_rel
}.