proposition: Lemma subst_steps sigma sigma' M : (forall n, clos_refl_trans _ step (sigma n) (sigma' n)) -> clos_refl_trans _ step (subst sigma M) (subst sigma' M).
proof: Proof. elim: M sigma sigma'. - move=> ???. by apply. - move=> * /=. apply: rt_trans; [apply: rt_stepsAppR|apply: rt_stepsAppL]; by auto. - move=> ? IH * /=. apply: rt_stepsLam. apply: IH. move=> [|?] /=; [by apply rt_refl|]. by apply: ren_steps. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect