proposition: Lemma par2dot F G: input F = output -> input G = output -> F ∥ G ≃2 F · G.
proof: Proof. intros HF HG. apply merge2_same; rewrite !HF !HG //. 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)