proposition: Lemma union_equiv_l_eqv_clot (A B: finType) (l: pairs A): union_equiv_l B (eqv_clot l) =2 eqv_clot (map_pairs inl l).
proof: Proof. rewrite /union_equiv_l/=/union_equiv_l_rel. move => [x|x] [y|y]. + rewrite (@eqv_clot_map _ _ _ _ _ (@inl A B)) //. exact: inl_inj. + by rewrite eqv_clot_map_lr. + by rewrite equiv_sym eqv_clot_map_lr. + by rewrite eqv_clot_map_eq ?sum_eqE // inr_codom_inl. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)