proposition: Lemma par2edgeunit a u b c: edge_graph2 a u b ∥ unit_graph2 c ≃2 unit_graph2 (a⊗(b⊗c)) ∔ [tt, u, tt].
proof: Proof. unshelve Iso2 (@merge_surj _ _ (edge_graph2 a u b ⊎ unit_graph2 c) _ (unit_graph2 (a⊗(b⊗c)) ∔ [tt, u, tt]) (fun _ => tt) (fun _ => inr tt) (bij_comp sumxU (option_bij sumxU)) xpred0 _ _ _). - apply kernel_eqv_clot. + by repeat constructor. + (repeat case)=>//=_; try eqv; apply eqv_clot_trans with (inr tt); eqv. - by case. - split. + move=>d. by repeat case. + repeat case=>//=. by rewrite eqxx /= !big_sumType !big_unitType monA. + 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 ptt)