proposition: Lemma step_halt_cbn s t ts ctx : closed s -> step s t -> halt_cbn ts ctx t -> halt_cbn ts ctx s.
proof: Proof. move=> Hs Hst. elim: Hst Hs ts ctx; clear s t. - move=> s t /closed_app [Hs Ht] ts ctx H'. apply: halt_app. apply: halt_lam_ts. apply: (halt_cbn_flatten_iff H'); first done. rewrite /= !simpl_term /=. apply: ext_subst_term. move=> [|n] /=; last done. rewrite !simpl_term. apply: ext_subst_term. move=> n /=. by rewrite !simpl_term. - move=> s s' t ? IH /closed_app [Hs Ht] ts ctx /halt_cbnE /IH {}IH. apply: halt_app. by apply: IH. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect