Add Eqb class, rewrite dbs, and some tactics from Pyrosome

[DIJamner]

Adds an Eqb class for types with boolean equality, a set of lemmas gathered into a rewrite database for greedy proposition simplification, another rewrite database for datatype inversion, and some generic tactics for inversion and case analysis.

[samuelgruetter]

Nice! Your comments caution against DecidableEq, and I agree with them. Does your code actually use DecidableEq at all? If not, I could also imagine having this code here without DecidableEq.

[DIJamner]

Since you're right that we shouldn't encourage its use, I moved DecidableEq back to Pyrosome for now. I'm not using it for much anymore, but I'll keep it in my project code base for now.