proposition: Lemma rt_stepsAppL M M' N :rt_steps M M' -> rt_steps (app M N) (app M' N).
proof: Proof. by elim; eauto using clos_refl_trans, step. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect