proposition: Lemma var_freshes : forall L n, { xs : list var | fresh L n xs }.
proof: Proof. Proof using. intros. gen L. induction n; intros L. exists* (nil : list var). destruct (var_fresh L) as [x Fr]. destruct (IHn (L \u \{x})) as [xs Frs]. exists* (x::xs). Qed.
imports: TLC(LibTactics LibList LibLogic LibNat LibEpsilon LibReflect)