proposition: Lemma rt_stepsAppR M N N' : rt_steps N N' -> 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