proposition: Lemma inverse_simulation s t : clos_refl_trans step (colon s (lam (var 0))) (lam t) -> closed s -> exists t', eval s t'.
proof: Proof. move=> /terminating_Acc /(Acc_clos_trans term). move Es': (colon s (lam (var 0))) => s' Hs'. elim: Hs' s Es' => {}s' _ IH s ? Hs. subst s'. suff : exists t', star L_facts.step s (lam t'). { move=> [t' ?]. by exists (lam t'). } case: (cbv_step_lam_or_progress Hs). { move=> [t' ->]. exists t'. by apply: starR. } move=> [s'] /[dup] /cbv_step_L_step /(_ Hs) H0s. move=> /[dup] /simulate_cbv_step /(_ Hs (lam (var 0))) /clos_trans_swap /IH H1s. move=> /cbv_step_closed /(_ Hs) /H1s => /(_ eq_refl) [? [Hs't']] [t' ?]. subst. exists t'. by apply: starC; eassumption. 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)