proposition: Lemma eval_cbv_steps s t : L.eval s t -> closed s -> clos_refl_trans cbv_step s t.
proof: Proof. elim; clear s t. { move=> *. by apply: rt_refl. } move=> s u t t' v Hsu IH1 Htt' IH2 Hv IH3 /closed_app [Hs Ht]. move: (Hs) => /IH1 => - {}IH1. move: (Ht) => /IH2 => - {}IH2. have Ht' : closed t' by (apply: closed_eval; eassumption). have Hu : bound 1 u. { by have /closed_dcl /boundE := closed_eval Hsu Hs. } have /IH3 {}IH3 : closed (L.subst u 0 t'). { apply /closed_dcl. apply: closed_subst; [done|by apply /closed_dcl]. } move: IH3. have -> : L.subst u 0 t' = subst (scons t' var) u. { rewrite L_subst_Lambda_subst; first done. apply: (bound_ext_subst_term Hu). move=> [|n]; [done|lia]. } move=> {}IH3. apply: rt_trans. { apply: cbv_steps_appL. eassumption. } apply: rt_trans. { apply: cbv_steps_appR. eassumption. } apply: rt_trans; last by eassumption. move: Htt' => /eval_iff [_] [? ->]. apply: rt_step. by apply: cbv_step_lam. 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)