proposition: Lemma union_merge_lEl (x: F): union_merge_l (@unl _ _ (merge_seq F l) _ (\pi x)) = \pi unl x.
proof: Proof. by rewrite /=union_quot_lEl quot_sameE. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)