proposition: Lemma union_merge_rEl (x: F): union_merge_r (unl x) = \pi (unl x).
proof: Proof. rewrite /=. rewrite (union_merge_lEr _ x) . rewrite (merge_isoE (union_C G F) _ (unr x)). by rewrite merge_sameE. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)