proposition: Lemma Krivine_step_halt_cbn ts ctx t ctx' t' : clos_refl_trans _ Krivine_step (ts, ctx, t) (nil, ctx', lam t') -> halt_cbn ts ctx t.
proof: Proof. move=> /clos_rt_rt1n_iff. move E: ([], ctx', lam t') => x H. change (halt_cbn ts ctx t) with (halt_cbn (fst (fst (ts, ctx, t))) (snd (fst (ts, ctx, t))) (snd (ts, ctx, t))). elim: H E. - move=> ? <-. by constructor. - move=> > H _ IH ?. subst. case: H IH=> > /(_ eq_refl) ?; by constructor. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect