proposition: Lemma halt_cbn_Krivine_step ts ctx t : halt_cbn ts ctx t -> exists ctx' t', clos_refl_trans _ Krivine_step (ts, ctx, t) (nil, ctx', lam t').
proof: Proof. elim. - move=> > ? [?] [?] ?. do 2 eexists. apply: rt_trans; [apply: rt_step; by constructor|eassumption]. - move=> > ? [?] [?] ?. do 2 eexists. apply: rt_trans; [apply: rt_step; by constructor|eassumption]. - move=> > ? [?] [?] ?. do 2 eexists. apply: rt_trans; [apply: rt_step; by constructor|eassumption]. - move=> > ? [?] [?] ?. do 2 eexists. apply: rt_trans; [apply: rt_step; by constructor|eassumption]. - move=> >. do 2 eexists. by apply: rt_refl. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect