proposition: Lemma simulation {s t} : L.eval s t -> closed s -> forall x, clos_refl_trans step (colon s x) (colon t x).
proof: Proof. move=> /eval_cbv_steps + /[dup] => /[apply]. elim. - move=> > /simulate_cbv_step /[apply] H x. by apply: clos_t_rt. - move=> *. by apply: rt_refl. - move=> *. apply: rt_trans; by eauto using cbv_steps_closed. 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)