proposition: Lemma union_merge_lEr (x: G): union_merge_l (unr x) = \pi unr x.
proof: Proof. by rewrite /=union_quot_lEr quot_sameE. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)