proposition: Lemma step'_machine s t vs y : step' s t -> closed s -> Forall eclosed_future vs -> machine (closure [] t) vs y -> exists y', flatten y' = flatten y /\ machine (closure [] s) vs y'.
proof: Proof. move=> H. elim: H vs y. - move=> {}s {}t vs y /closed_app [/closed_dcl /boundE Hs /closed_dcl Ht] Hvs IH. have : flatten (closure [] (subst s 0 (lam t))) = flatten (closure [closure [] (lam t)] s). { rewrite /flatten -/flatten /= !flatten_term subst_many_nil. by apply: subst_subst_many_single. } move: IH => /machine_flatten_equiv /[apply] => /(_ vs). apply: unnest. { by split; [apply: closed_subst|]. } apply: unnest. { done. } move=> /(_ Hvs Hvs erefl) [y' [? ?]]. exists y'. split; [done|]. apply: machine_app. apply: machine_lam_swap. by apply: machine_lam_subst. - move=> {}s {}t u ? IH vs y /closed_app [Hs Ht] Hvs. move=> /machineE /machineE /(IH _ y Ht). apply: unnest. { constructor; [|done]. by split; [apply /closed_dcl|]. } move=> [y'] [??]. exists y'. split; [done|]. apply: machine_app. by apply: machine_lam_swap. - move=> {}s {}t u ? IH vs y /closed_app [Hs ?] Hvs. move=> /machineE /(IH _ y Hs). apply: unnest. { constructor; [|done]. by split; [apply /closed_dcl|]. } move=> [y'] [??]. exists y'. by split; [|apply: machine_app]. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun