Less eta-equality for algebraic structures

[felixwellen]

Use "no-eta-equality" for the records defining algebraic structures. @plt-amy helped :-)

[felixwellen]

This might be feasible, but I still don't see, if this will really help to fix type checking speed problems. I'll not continue on this for now, but might try it again, when I'm really bothered by speed problems.