proposition: Lemma fresh_empty : forall L n xs, fresh L n xs -> fresh \{} n xs.
proof: Proof. Proof using. intros. rewrite <- (union_empty_r L) in H. destruct* (fresh_union_r _ _ _ _ H). Qed.
imports: TLC(LibTactics LibList LibLogic LibNat LibEpsilon LibReflect)