proposition: Lemma flatten_closure_var_S x xs n : n < length xs -> flatten (closure (x :: xs) (var (S n))) = flatten (closure xs (var n)).
proof: Proof. move=> ?. rewrite !flatten_var /=. apply: nth_indep. by rewrite map_length. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun