Computing the free variables of a term.
 data FreeVars = FV {}
 class Free a
 freeVars :: Free a => a > FreeVars
 allVars :: FreeVars > VarSet
 relevantVars :: FreeVars > VarSet
 rigidVars :: FreeVars > VarSet
 freeIn :: Free a => Nat > a > Bool
 isBinderUsed :: Free a => Abs a > Bool
 freeInIgnoringSorts :: Free a => Nat > a > Bool
 relevantIn :: Free a => Nat > a > Bool
 data Occurrence
 = NoOccurrence
  StronglyRigid
  WeaklyRigid
  Flexible
 occurrence :: Nat > FreeVars > Occurrence
Documentation
The distinction between rigid and strongly rigid occurrences comes from: Jason C. Reed, PhD thesis, 2009, page 96 (see also his LFMTP 2009 paper)
The main idea is that x = t(x) is unsolvable if x occurs strongly rigidly in t. It might have a solution if the occurrence is not strongly rigid, e.g.
x = f > suc (f (x ( y > k))) has x = f > suc (f (suc k))
 Jason C. Reed, PhD thesis, page 106
Free variables of a term, (disjointly) partitioned into strongly and and weakly rigid variables, flexible variables and irrelevant variables.
FV  

freeVars :: Free a => a > FreeVarsSource
Doesn't go inside solved metas, but collects the variables from a
metavariable application X ts
as flexibleVars
.
relevantVars :: FreeVars > VarSetSource
All but the irrelevant variables.
isBinderUsed :: Free a => Abs a > BoolSource
Is the variable bound by the abstraction actually used?
freeInIgnoringSorts :: Free a => Nat > a > BoolSource
relevantIn :: Free a => Nat > a > BoolSource
occurrence :: Nat > FreeVars > OccurrenceSource
occurrence x fv
ignores irrelevant variables in fv