hasFV :: Term -> [String] -> Bool
hasFV (TmVar v)     vl = not (v `elem` vl)
hasFV (TmAbs v t)   vl = hasFV t (v:vl)
hasFV (TmApp t1 t2) vl = hasFV t1 vl || hasFV t2 vl