added check to avoid eta-expansion when both terms are lambdas, and removed the check in eta-expansion that ensures the other side is a function, and added unification of types in let-same.  now it compiles 49 files of ssreflect