fact: Fixpoint FreshDistinctVars (T :VarType) (lv :list (typ T)) (lvAvoid :list (typ T)) {struct lv} : (list (typ T)) := match lv with | [] => [] | vh :: vtl => let newvar := ((fresh T) lvAvoid [vh]) in newvar :: (FreshDistinctVars T vtl (newvar :: lvAvoid)) end.
imports: AssociationList Omega