proposition: Lemma dot2unit_r' (G: graph2) a: G · unit_graph2 a ≃2 G [tst output <- a].
proof: Proof. unshelve Iso2 (@merge_surj _ _ (G ⊎ unit_graph2 a) _ (G [tst output <- a]) (fun x => match x with inl y => y | inr tt => output end) (fun x => unl x) sumxU xpred0 _ _ _). 4,5: by rewrite merge_surjE. - apply kernel_eqv_clot. * by constructor. * case=>[x|[]]; case=>[y|[]]=>//->; eqv. - by []. - split. + by move=> [e|[]] b. + move=>x/=. rewrite big_sumType big_pred1_eq. case: (altP (x =P output)) => [?|xDo]; subst. * by rewrite (big_pred1 tt) => [|[]]; rewrite 1?monC /= ?eqxx. * rewrite big_pred0 ?monU // => [[]]. by rewrite eq_sym (negbTE xDo). + by case. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)