proposition: Lemma merge_subgraph_isoE x0 : (forall x, merge_subgraph_iso (\pi (inl x)) = \pi (insubd x0 (val x))) * (forall y, merge_subgraph_iso (\pi (inr y)) = \pi (insubd x0 (val y))).
proof: Proof. split => [x|y]. all: rewrite /= !quot_sameE. all: apply/eqquotP; rewrite -eqv_clot_union_rel; apply/eqquotP. all: symmetry; rewrite -merge_union_can'; apply: merge_union_fwd_hom => //. all: rewrite reprK /merge_union_bwd. - case: setU_dec; rewrite val_insubd !inE !(valP x) //=. 2: by case. move => a. by rewrite valK'. - case: setU_dec; rewrite !val_insubd !inE !(valP y) !orbT //=. + move => a. by rewrite -{2}[y]valK' ?(valP y). + case => a b /=. by rewrite valK'. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)