proposition: Lemma par_edges (a b c d: Lv) (u v: Le): point (merge_seq (edge_graph a u b ⊎ edge_graph c v d) [:: (inl (inl tt), inr (inl tt)); (inl (inr tt), inr (inr tt))]) (\pi inl (inl tt)) (\pi (inr (inr tt))) ≃2 two_graph2 (a⊗c) (b⊗d) ∔ [inl tt, u, inr tt] ∔ [inl tt, v, inr tt].
proof: Proof. unshelve Iso2 (@merge_surj _ _ (edge_graph a u b ⊎ edge_graph c v d) _ (two_graph2 (a⊗c) (b⊗d) ∔ [_, u, _] ∔ [_, v, _]) (fun x => match x with | inl y => y | inr y => y end) (inl) (two_option_void') xpred0 _ _ _ ). 4,5: apply merge_surjE. - apply kernel_eqv_clot. * by repeat constructor. * case=>[[[]|[]]|[[]|[]]]; case=>[[[]|[]]|[[]|[]]]//= _; eqv. - by repeat case. - split. + by repeat case. + move => y. rewrite !big_sumType !big_unitType. by case: y => [[]|[]] /=; rewrite ?monU ?monUl. + by repeat case. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)