fact: Definition eqv_ (X: elabelType) (b: bool) (x y: X) := if b then x ≡' y else x ≡ y.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop bij)