proposition: Lemma ren_step xi M M' : step M M' -> step (ren xi M) (ren xi M').
proof: Proof. move=> H. elim: H xi; [|by eauto using step..]. move=> > /=. apply: P_equal; [by apply: stepSubst|]. rewrite !simpl_term. apply: ext_subst_term. by case. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect