Add options to ho_unifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Remove duplicate solutions in the higher order matching module. Simplify solutions when higher-order matching is used, and we don't have a residue.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>