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: <A href="cic:/matita/ng/properties/relations/reflexive.def(1)">reflexive</A> ? eq_rel;
+ sym: <A href="cic:/matita/ng/properties/relations/symmetric.def(1)">symmetric</A> ? eq_rel;
+ trans: <A href="cic:/matita/ng/properties/relations/transitive.def(1)">transitive</A> ? eq_rel
}.