proposition: Lemma stepsApp M1 M2 N : steps M1 M2 -> steps (app M1 N) (app M2 N).
proof: Proof. elim=> *. - apply: rt_step. by apply: wCBN_stepApp. - apply: rt_refl. - by apply: rt_trans; eassumption. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts) Undecidability.L.Util.L_facts Relations Lia ssreflect