Some files ported to intermediate syntax to test.

[helm.git] / matita / matita / nlibrary / properties / relations.ma

diff --git a/matita/matita/nlibrary/properties/relations.ma b/matita/matita/nlibrary/properties/relations.ma
index 581208d9afb8fcf567a4f931b8fe16f6899edeb2..1df2e205a5d097a2680ad0864d92145ada7c9906 100644 (file)
--- a/matita/matita/nlibrary/properties/relations.ma
+++ b/matita/matita/nlibrary/properties/relations.ma
@@ -14,11 +14,11 @@
 
 include "logic/pts.ma".
 
-ndefinition reflexive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x.P x x.
-ndefinition symmetric ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x,y.P x y → P y x.
-ndefinition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z → P z y → P x y.
+definition reflexive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x.P x x.
+definition symmetric ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x,y.P x y → P y x.
+definition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z → P z y → P x y.
 
-nrecord equivalence_relation (A:Type[0]) : Type[1] ≝
+record equivalence_relation (A:Type[0]) : Type[1] ≝
  { eq_rel:2> A → A → CProp[0];
    refl: reflexive ? eq_rel;
    sym: symmetric ? eq_rel;