proposition: Lemma equivalence_equivalence r: equivalence r -> equivalence_re (related r)(substrate r).
proof: Proof. move => [gr ra rb rc]; split => // y. by split => p; [ apply: ra | substr_tac ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)