proposition: Lemma flatten_closure_var_bound xs x : (if flatten (closure xs (var x)) is var _ then False else True) -> x < length xs.
proof: Proof. rewrite flatten_var. move=> H. suff: not (length xs <= x) by lia. move=> ?. by rewrite nth_overflow in H; [rewrite map_length|]. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun