proposition: Lemma cbv_step_lam_or_progress {s} : closed s -> (exists s', s = lam s') \/ (exists t, cbv_step s t).
proof: Proof. elim: s. - by move=> ? /not_closed_var. - move=> s IHs t IHt /closed_app [/IHs {}IHs /IHt {}IHt]. right. case: IHs; case: IHt. + move=> [? ->] [? ->]. eexists. by apply: cbv_step_lam. + move=> [? ?] [? ->]. eexists. apply: cbv_step_appR. by eassumption. + move=> [? ->] [? ?]. eexists. apply: cbv_step_appL. by eassumption. + move=> [? ?] [? ?]. eexists. apply: cbv_step_appL. by eassumption. - move=> *. left. by eexists. 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)