proposition: Lemma cbv_step_L_step s s' : cbv_step s s' -> closed s -> L_facts.step s s'.
proof: Proof. elim; clear s s'. - move=> s s' /closed_app [/closed_dcl /boundE ?] /closed_dcl ?. have := L_facts.stepApp s s'. congr L_facts.step. rewrite L_subst_Lambda_subst. { by apply /closed_dcl. } apply: bound_ext_subst_term; first by eassumption. move=> [|n]; [done|lia]. - move=> > ? H /closed_app [/H ? ?]. by apply: stepAppL. - move=> > ? H /closed_app [? /H ?]. by apply: stepAppR. 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)