proposition: Lemma fresh_single_notin : forall x xs n, fresh \{x} n xs -> x \notin from_list xs.
proof: Proof. Proof using. induction xs; destruct n; introv F; simpl in F; tryfalse. rewrite~ from_list_nil. destruct F as [Fr F']. lets [? ?]: (fresh_union_r F'). specializes IHxs n. rewrite~ from_list_cons. Qed.
imports: TLC(LibTactics LibList LibLogic LibNat LibEpsilon LibReflect)