fact: Fixpoint fresh_list (L : t) (n : nat) (xs : list X.t) {struct xs} : Prop := match xs, n with | nil, O => True | cons x xs', S n' => notin x L /\ fresh_list (union L (singleton x)) n' xs' | _, _ => False end.
imports: Coq.FSets.FSets Metalib.CoqFSetInterface