proposition: Lemma step_IO G G': step G G' -> (input == output :> G) = (input == output :> G').
proof: Proof. by case. 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)