proposition: Lemma Krivine_step_halt_cbn_step ts ctx t ts' ctx' t' : Krivine_step (ts, ctx, t) (ts', ctx', t') -> halt_cbn ts' ctx' t' -> halt_cbn ts ctx t.
proof: Proof. move EX: (ts, ctx, t) => X. move EY: (ts', ctx', t') => Y H. case: H EX EY=> > [-> -> ->] [] *; subst. all: by constructor. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect