proposition: Lemma simulate_cbv_step s s' : cbv_step s s' -> closed s -> forall x, clos_trans step (colon s x) (colon s' x).
proof: Proof. elim; clear s s'. - move=> s t /closed_app [? ?]. move=> ?. by apply: colon_redex. - move=> s s' t Hss' IH /closed_app [/[dup] /IH {}IH Hs Ht]. have [s1 [s2 ?]] : exists s1 s2, s = app s1 s2. { by case: Hss' => *; eexists; eexists. } subst s. rewrite /=. move: s' IH Hss' => []. + by move=> ? ? /cbv_step_closed /(_ Hs) /not_closed_var. + move=> s'1 s'2 IH Hss' x. by apply: IH. + move=> s' IH /cbv_step_to_lam [s1'] [s2'] [? [? Hs']]. move=> x. subst. apply: t_trans. { by apply: IH. } apply: t_trans. { apply: t_step. by apply: wCBN_stepSubst. } have := steps_to_colon t (lam (app (app (ren S (Psi (lam s'))) # 0) (ren S x))) Ht. by rewrite /= !simpl_term !ren_as_subst_term. - move=> > ? IH /closed_app [? /IH] {}IH x. by apply: IH. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)