proposition: Lemma eqv_clot_map_lr (F G : finType) (l : pairs F) x y : eqv_clot (map_pairs inl l) (@inl F G x) (@inr F G y) = false.
proof: Proof. rewrite (@eqv_clot_mapF _) ?inr_codom_inl //. exact: inl_inj. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)