proposition: Lemma par_steps_l G G' H: steps G G' -> steps (G∥H) (G'∥H).
proof: Proof. apply (step_to_steps (f:=fun G => (G∥H))) => {G G'}. - move => G G' I; exact: par_eqv. - move => G G' step_G_G'. etransitivity. apply: (@merge_step G') => //=. + by rewrite /admissible_l/= !inE !eqxx. + rewrite /replace_ioL/= !eqxx. case: ifP => [E|//]. rewrite (step_IO step_G_G') in E. by rewrite -[in (inl output,inr input)](eqP E). Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)