proposition: Lemma inverse_simulation ts ctx s : halt_cbn ts ctx s -> exists t', clos_refl_trans step (many_app (flatten (closure ctx s)) (map flatten ts)) (lam t').
proof: Proof. elim. - move=> > ? [t'] /= Ht'. exists t'. move: Ht'. congr clos_refl_trans. congr fold_left. rewrite !simpl_term. apply: ext_subst_term => n. by rewrite /= !simpl_term. - done. - done. - move=> [? ?] > ? [t'] /= Ht'. exists t'. apply: rt_trans; last by eassumption. apply: rt_step. apply: step_many_app. apply: stepLam'. rewrite !simpl_term /=. apply: ext_subst_term. move=> [|n] /=. + rewrite !simpl_term. apply: ext_subst_term => n. by rewrite /= !simpl_term. + by rewrite !simpl_term ren_as_subst_term. - move=> >. eexists. by apply: rt_refl. Qed.
imports: Undecidability.LambdaCalculus(Lambda Krivine Util.term_facts Util.wCBN_facts Util.Krivine_facts) List Relations ssreflect