proposition: Lemma nsteps_congruence {B} (f : A → B) (R' : relation B) n x y : (∀ x y, R x y → R' (f x) (f y)) → nsteps R n x y → nsteps R' n (f x) (f y).
proof: Proof. induction 2; econstructor; eauto. Qed.
imports: stdpp(options)