proposition: Lemma merge_subgraph_hom : is_ihom merge_subgraph_v merge_subgraph_e xpred0.
proof: Proof. rewrite /merge_subgraph_e /merge_subgraph_v. split=>//. - case=> x b /=; rewrite merge_unionE quot_sameE; congr pi; exact: val_inj. - case=> e //. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)