proposition: Lemma subst_step M N sigma : step M N -> step (subst sigma M) (subst sigma N).
proof: Proof. move=> H. elim: H sigma; [|by eauto using step..]. move=> > /=. apply: P_equal; [apply: stepSubst|]. rewrite !simpl_term. apply: ext_subst_term=> - [|?]; [done|]. by rewrite /= !simpl_term. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect