Avoid decidable equality for type indices in binary op case of symbolic term equality function

[skeuchel]

In our function for testing for equality of two symbolic terms of the same type, https://github.com/katamaran-project/katamaran/blob/26a30b5b62d98f76aca01c7c06611b3fe0199a6c/theories/Syntax/Terms.v#L296-L322 we throw exactly that information away in the binary op case and rather implement fully heterogenous decidable equality for binops https://github.com/katamaran-project/katamaran/blob/26a30b5b62d98f76aca01c7c06611b3fe0199a6c/theories/Syntax/BinOps.v#L145-L147 which for instance tests equality of the components of a product type, even if we already knew that the results, i.e. the product types, were equal! https://github.com/katamaran-project/katamaran/blob/26a30b5b62d98f76aca01c7c06611b3fe0199a6c/theories/Syntax/BinOps.v#L156-L157

These additional equality checks of types, or more generally part of the type index of symbolic terms like for instance natural numbers for the bitvector length, can block metalevel computation when running the symbolic executor on polymorphic functions, i.e. functions with some form of quantification at the metalevel. For instance, the verification of the to_bits function from the RISC-V case study, critically relies on the fact that the term equality in the unary op case does not use decidable equality on the metalevel bitvector length https://github.com/katamaran-project/katamaran/blob/26a30b5b62d98f76aca01c7c06611b3fe0199a6c/case_study/RiscvPmp/Machine.v#L536-L537

The decidable equality check is correctly implemented for unary ops, i.e. we propagate the information that the result type of the two unary ops being compared is the same https://github.com/katamaran-project/katamaran/blob/26a30b5b62d98f76aca01c7c06611b3fe0199a6c/theories/Syntax/UnOps.v#L86-L88 I propose to implement the same for binary ops.

However, this is more difficult for binary ops because of the green slime in the indices https://github.com/katamaran-project/katamaran/blob/26a30b5b62d98f76aca01c7c06611b3fe0199a6c/theories/Syntax/BinOps.v#L81-L82

Trying to implement it in the same way as for unary ops using the equations package fails with an error message that a covering cannot be found.