Fix bug in ho_unifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Remove cleanup_subst. The residue may still reference auxiliary variable. So, it is not safe to remove then from the resultant partial substitution.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add imitation step for equalities.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add imitation for lambdas and Pis

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