proposition: Lemma var_gen_spec : forall E, (var_gen E) \notin E.
proof: Proof. intros E. assert (Hlt : forall n, n \in E -> n < var_gen E). { intros n H. induction E as [|x xs IHxs]; unfold var_gen in *; simpl in *; try (now exfalso; auto). destruct H; subst; rewrite Nat.succ_max_distr, Nat.max_lt_iff; auto. } intros contra. apply Hlt in contra. lia. Qed.
imports: Equations(Equations) Arith List ListSet Lia Program