Improve higher order unification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix abuse of operator-> overload

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix memory corruption bug

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix bug in the type checker (when type checking terms with meta-variables).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add rewrite and first-order pattern matching skeletal
Update fo_match
Add then and orelse rewrite combinators and tests