proposition: Lemma machine_var_bound xs x vs y : machine (closure xs (var x)) vs y -> x < length xs.
proof: Proof. elim: x xs. - move=> [|??] /machineE /=; lia. - move=> ? IH [|??] /machineE; [done|]. move=> /IH /=. lia. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun