proposition: Lemma g2_A12' (F G: graph2): input F = output F -> F·G ≃2 F·top ∥ G.
proof: Proof. intro H. irewrite' (merge_iso2 (union_merge_l _ _)). rewrite /map_pairs/map 2!union_merge_lEl 2!union_merge_lEr /=. irewrite' (merge_merge (G:=(F ⊎ g2_top) ⊎ G) (k:=[::(inl (inl input),inr input);(inl (inr (inr tt)),inr output)])) =>//. irewrite' (merge_iso2 (union_C (_ ⊎ _) _)). irewrite' (merge_iso2 (union_A _ _ _))=>/=. irewrite' (merge_union_K_l (F:=G ⊎ F) (K:=g2_top) _ _ (k:=fun x => if x then unr input else unl output))=>//. 2: by case. 2: by repeat case; apply /eqquotP; rewrite H; eqv. irewrite (merge_iso2 (union_C F G)) =>/=. apply merge_same'. rewrite H. apply eqv_clot_eq; leqv. repeat case=>//=; rewrite H; apply /eqquotP; eqv. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)