proposition: Lemma pi_hom (G : graph) (e : equiv_rel G) : hom_s (pi e : skeleton G -> skeleton (merge G e)).
proof: Proof. move => x y xy Dxy. apply/sk_rel_mergeE. split => //. by exists x; exists y. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)