proposition: Lemma fresh_not_in : forall l, ~ In (fresh l) l.
proof: Proof. intro l. unfold fresh. destruct atom_fresh_for_list. auto. Qed.
imports: Coq.Arith.Arith Coq.Arith.Max Coq.Classes.EquivDec Coq.Lists.List Coq.Structures.Equalities Coq.FSets.FSets Metalib.CoqListFacts Metalib.FSetExtra Metalib.FSetWeakNotin Metalib.LibTactics Lia