• Perhaps I just don't see the trivial way to use Higher-Order Unification as a means to find solutions to this. For instance $len (xs ++ ys) = (len xs) + (len ys)$. This is clearly easy to find a counter example to (constant 1 function) but I don't see how higher order unification helps me with that. – Jake Dec 9 '14 at 0:19
• $\newcommand\doubleplus{+\kern-1.3ex+\kern0.8ex}$ looks like the latex came out really bad this looks better: $len(xs \doubleplus ys) = len\,\,xs + len\,\,ys$ – Jake Dec 9 '14 at 2:21