Program transformation ideas

From watching Ian write Agda in Emacs

• quantify over all of the free variables in the current term
• thread new arguments through all of the patterns / recursive calls (and also when removed)
• figure out when an argument is not actually used in any non-trivial way