Corrected some bugs in goal solving and elaboration, added tactics for solving unification problems. For now <= is treated as == in unification problems.