proposition: Lemma machine_simulation {s t} : L.eval s t -> closed s -> exists y, flatten y = t /\ machine (closure [] s) [] y.
proof: Proof. move=> /[dup] + /eval_is_lam [t']. move=> /eval_steps' /clos_rt_rt1n_iff. elim. { move=> ? -> ?. eexists. by split; [apply flatten_term|apply machine_lam]. } move=> {}s u {}t /[dup] /step'_machine Hsu /step'_closed H'su _ /[apply]. move=> + /[dup] /H'su => /[apply] - [y] [<-]. move=> /Hsu /[apply]. by apply. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun