proposition: Lemma eqv10 (l : elabelType) (x y z : l) : eqv' x y -> eqv y z -> eqv' x z.
proof: Proof. move => /Eqv'_sym A B. apply: Eqv'_sym. apply: eqv01 A. by symmetry. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop bij)