fact: Definition fresh (l : list atom) := match atom_fresh_for_list l with (exist _ x _) => x end.
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