proposition: Lemma simulation s t ts ctx : clos_refl_trans step s t -> closed s -> halt_cbn ts ctx t -> halt_cbn ts ctx s.
proof: Proof. move=> /(clos_rt_rt1n term). elim; [done|]. move=> > /[dup] /step_closed ? /step_halt_cbn. by auto with nocore. Qed.
imports: Undecidability.LambdaCalculus(Lambda Krivine Util.term_facts Util.wCBN_facts Util.Krivine_facts) List Relations ssreflect