Improve treatment of l == r case in EqProver

Not sure that it has positive effect.
Implemented generalizer

It works more or less but it's not used for anything yet.