proposition: Lemma step_ren xi M N : step M N -> step (ren xi M) (ren xi N).
proof: Proof. move=> H. elim: H xi. { move=> > /=. apply: stepSubst'. rewrite !simpl_term. apply: ext_subst_term. by case. } all: by eauto using step with nocore. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect