proposition: Lemma cbv_steps_appR {s t t'} : clos_refl_trans cbv_step t t' -> clos_refl_trans cbv_step (app (lam s) t) (app (lam s) t').
proof: Proof. elim; by eauto using @clos_refl_trans, cbv_step with nocore. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)