proposition: Lemma relabel2_dot (F G: graph2 Lv1 Le1): relabel2 (F · G) ≃2 relabel2 F · relabel2 G.
proof: Proof. etransitivity. apply (iso_iso2 (relabel_merge _)). refine (merge_iso2 (relabel_union F G) _ _ _). Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)