proposition: Lemma par2A (F G H: graph2): F ∥ (G ∥ H) ≃2 (F ∥ G) ∥ H.
proof: Proof. irewrite (merge_iso2 (union_merge_r _ _)). rewrite /map_pairs/map 2!union_merge_rEl 2!union_merge_rEr /=. irewrite (merge_merge (G:=F ⊎ (G ⊎ H)) (k:=[::(unl input,unr (unl input)); (unl output,unr (unr output))]))=>//. irewrite' (merge_iso2 (union_merge_l _ _)). rewrite /map_pairs/map 2!union_merge_lEl 2!union_merge_lEr /=. irewrite' (merge_merge (G:=(F ⊎ G) ⊎ H) (k:=[::(unl (unl input),unr input); (unl (unr output),unr output)]))=>//. irewrite (merge_iso2 (union_A _ _ _)). apply merge_same'. rewrite /unl/unr/=. set a := inl _. set (b := inl _). set (c := inl _). set (d := inl _). set (e := inr _). set (f := inr _). apply eqv_clot_eq=>/=. constructor. apply eqv_clot_trans with c; eqv. constructor. apply eqv_clot_trans with b; eqv. constructor. eqv. constructor. apply eqv_clot_trans with b; eqv. leqv. constructor. eqv. constructor. apply eqv_clot_trans with f; eqv. constructor. apply eqv_clot_trans with a; eqv. 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)