proposition: Lemma step_to_steps f: Proper (eqv ==> eqv) f -> Proper (step ==> steps) f -> Proper (steps ==> steps) f.
proof: Proof. intros If Sf G G' S. induction S as [G G' I|G G' F H' I S Ss IH]. - by apply isop_step, If. - etransitivity. apply isop_step, If. exists. apply I. etransitivity. apply Sf, S. apply IH. 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)