proposition: Lemma dot2A (F G H: graph2): F · (G · H) ≃2 (F · G) · H.
proof: Proof. irewrite dot2Aflat. irewrite' (merge_iso2 (union_merge_l _ _)). rewrite /map_pairs/map 2!union_merge_lEl 2!union_merge_lEr /fst/snd. irewrite' (merge_merge (G:=(F ⊎ G) ⊎ H) (k:=[::(unl (unr output),unr input)])) =>//. irewrite (merge_iso2 (union_A _ _ _)). apply merge_same'=>/=. apply eqv_clot_eq; leqv. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)