proposition: Lemma cbv_steps_appL {s s' t} : clos_refl_trans cbv_step s s' -> clos_refl_trans cbv_step (app s t) (app 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)