proposition: Lemma cbv_step_closed {s s'} : cbv_step s s' -> closed s -> closed s'.
proof: Proof. elim. - move=> > /closed_app [/closed_dcl /boundE ?] /closed_dcl ?. apply /closed_dcl. apply: bound_subst; first by eassumption. move=> [|n]; [done|lia]. - move=> > ? H /closed_app [/H ? ?]. by apply: app_closed. - move=> > ? H /closed_app [? /H ?]. by apply: app_closed; [|]. 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)