fact: Fixpoint fresh_distinct_vars (n:nat) (lv_avoid : list NVar) : (list NVar) := match n with | O => [] | S m => let newvar := fresh_var lv_avoid in newvar :: (fresh_distinct_vars m (newvar :: lv_avoid)) end.
imports: list Omega