proposition: Lemma enc_halt_cbn_app_spec ts ctx s t rec : normal_form rec -> (forall xi, ren xi rec = rec) -> (forall sigma, subst sigma rec = rec) -> clos_refl_trans _ step' (many_app enc_halt_cbn_app [enc_list enc_eterm ts; enc_list enc_eterm ctx; enc_term s; enc_term t; rec; I]) (many_app rec [enc_list enc_eterm ((closure ctx t)::ts); enc_list enc_eterm ctx; enc_term s; rec; I]).
proof: Proof. move=> H1r H2r H3r. do ? (apply: rt_step'; [by do ? constructor|]; rewrite /= ?subst_enc ?H2r ?H3r). by apply: rt_refl. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect