Do not merge (yet).

This is an experiment if we can make kernel reduction of the Fin counterexamples faster if we optimize the terms for kernel reduction, removing all overhead due to type classes and Fin.

Before:

$ echo 'def recompileMePlease := 1' >> equational_theories/DecideBang.lean ; time lake build

real	4m56,266s
user	27m4,134s
sys	5m23,516s

After:

Build completed successfully.

real	5m49,879s
user	32m46,249s
sys	4m42,513s

Probably due to many many fast computations where just running it is faster
than optimizing it this way.

(The proofs therein are not very elegant, but I just wanted them done past 11pm…)