proposition: Lemma g2_A10 (F G: graph2): 1 ∥ F·G ≃2 dom (F ∥ G°).
proof: Proof. irewrite (par2C 1). irewrite (merge_iso2 (union_merge_l _ _)). rewrite /map_pairs/map 2!union_merge_lEl 1!union_merge_lEr /fst/snd. irewrite (merge_merge (G:=(F ⊎ G) ⊎ g2_one) (k:=[::(unl (unl input),inr tt); (unl (unr output),inr tt)])) =>//. irewrite (merge_union_K_l (F:=F ⊎ G) _ _ (k:=fun x => unl input))=>//=. 2: by intros []; apply /eqquotP; simpl; eqv. apply merge_same; simpl. apply eqv_clot_eq; simpl; leqv. eqv. 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)