proposition: Lemma dot2Aflat (F G H: graph2): F·(G·H) ≃2 point (merge_seq (F ⊎ (G ⊎ H)) [::(unr (unl output),unr (unr input)); (unl output,unr (unl input))]) (\pi unl input) (\pi unr (unr output)).
proof: Proof. irewrite (merge_iso2 (union_merge_r _ _)). rewrite /map_pairs/map 2!union_merge_rEl 2!union_merge_rEr /fst/snd. irewrite (merge_merge (G:=F ⊎ (G ⊎ H)) (k:=[::(unl output,unr (unl input))])) =>//. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)