proposition: Lemma dom2E (F: graph2): dom F ≃2 1 ∥ (F · top).
proof: Proof. symmetry. irewrite par2C. irewrite (merge_iso2 (union_merge_l _ _)). rewrite /map_pairs/map 2!union_merge_lEl 1!union_merge_lEr /=. irewrite (merge_merge (G:=(F ⊎ g2_top) ⊎ g2_one) (k:=[::(inl (inl input),inr tt); (inl (inr (inr tt)),inr tt)])) =>//. irewrite (merge_iso2 (iso_sym (union_A _ _ _))). irewrite (merge_union_K_l (K:=g2_top ⊎ g2_one) _ _ (k:=fun x => match x with inl (inl tt) => output | _ => input end))=>/=. apply merge_nothing. repeat (constructor =>//=). by intros [[]|]. by intros [[]|]. repeat case; apply /eqquotP; try eqv. apply eqv_clot_trans with (inr (inr tt)); 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)