proposition: Lemma closed_halt_iff {t} : closed t -> ((exists t', t = lam t') <-> (forall u, not (step t u))).
proof: Proof. intros Ht. split. { by move=> [? ->] ? /stepE. } suff: (forall s t, closed s -> closed t -> exists u, step (app s t) u). { case: t Ht. - by move=> ? /not_closed_var. - move=> s t /closed_app [++] H => /H /[apply]. by move=> [u] Hu /(_ u Hu). - move=> *. by eexists. } elim. - by move=> > /not_closed_var. - move=> ? IH1 ? IH2 ? /closed_app [/IH1] /[apply]. move=> [u Hu] ?. eexists. apply: wCBN_stepApp. by eassumption. - move=> *. eexists. by apply: wCBN_stepSubst. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts) Undecidability.L.Util.L_facts Relations Lia ssreflect