proposition: Lemma var_gen_spec : forall E, (var_gen E) \notin E.
proof: Proof. Proof using. intros. unfold var_gen. epsilon l. applys fset_finite. intros Hl. rewrite Hl. introv H. forwards M: var_gen_list_spec H. nat_math. Qed.
imports: TLC(LibTactics LibList LibLogic LibNat LibEpsilon LibReflect)