proposition: Lemma eclosed_var_S x xs n : eclosed (closure (x :: xs) (var (S n))) -> eclosed (closure xs (var n)).
proof: Proof. by move=> /= [/bound_var_S_iff ?] [??]. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun