proposition: Lemma halt_cbn_rt_step' ts ctx t : halt_cbn ts ctx t -> clos_refl_trans _ step' (enc_state ts ctx t) I.
proof: Proof. move=> /halt_cbn_Krivine_step. move=> [ctx'] [t'] /(clos_refl_trans_transport Krivine_step_steps' (sync_intro _ _ _)) [?] [/syncE] -> ?. apply: rt_trans; [eassumption|]. have := subst_enc_halt_cbn. have := ren_enc_halt_cbn. move E: enc_halt_cbn => rec. have H'rec : normal_form rec by (rewrite -E; do ? constructor). move=> H1rec H2rec. rewrite -[l in many_app l _]E /enc_halt_cbn. do ? (apply: rt_step'; [by do ? constructor|]; rewrite /= ?simpl_term ?H1rec ?H2rec). by apply: enc_halt_cbn_lam_spec'. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect