fact: Definition merge_subgraph_v : bij (merge_seq (G1 ⊎ G2) h) (merge_seq G12 h') := Eval hnf in (bij_comp (merge_union eqvI) (quot_same eqv_clot_union_rel)).
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)