proposition: Lemma eqv11 x y z: eqv' x y -> eqv' y z -> x ≡ z.
proof: Proof. move=> /= -> ->. apply cnvI. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures)