proposition: Lemma Krivine_step_steps' X Y X' : Krivine_step X Y -> sync X X' -> exists Y', steps' X' Y' /\ sync Y Y'.
proof: Proof. 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. case=> > /syncE ->; eexists; (split; [|by apply: sync_intro]); rewrite !E. all: rewrite -[l in steps' (many_app l _) _]E /enc_halt_cbn. - do ? ((apply: rt_step' || apply: t_step'); [by do ? constructor|]; rewrite /= ?simpl_term ?H1rec ?H2rec). by apply: enc_halt_cbn_var0_spec. - do ? ((apply: rt_step' || apply: t_step'); [by do ? constructor|]; rewrite /= ?simpl_term ?H1rec ?H2rec). by apply: enc_halt_cbn_varS_spec. - do ? ((apply: rt_step' || apply: t_step'); [by do ? constructor|]; rewrite /= ?simpl_term ?H1rec ?H2rec). by apply: enc_halt_cbn_app_spec. - do ? ((apply: rt_step' || apply: t_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