proposition: Lemma merge_add_vlabel (G: graph) (r: equiv_rel G) x a: merge (G [tst x <- a]) r ≃ merge G r [tst \pi x <- a].
proof: Proof. Iso bij_id bij_id xpred0. split=>//= v. case: (altP (v =P \pi x)) => [-> {v}|D]. - rewrite (bigD1 x) // [in X in _ ≡ X](bigD1 x) // ?eqxx monA. apply: mon_eqv => //. apply: eqv_bigr => y /andP [_ H]. by rewrite (negbTE H). - apply: (eqv_big_bij (f := bij_id)) => //. + exact: bij_perm_enum. + move => /= y /eqP ?. case: (altP (y =P x)) => // ?; subst. by rewrite eqxx in D. Defined.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)