proposition: Lemma ren_steps xi M M' : clos_refl_trans _ step M M' -> clos_refl_trans _ step (ren xi M) (ren xi M').
proof: Proof. by elim; eauto using clos_refl_trans, ren_step. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect