Avoid decidable equality for type indices in symbolic formula equality function

[skeuchel]

For the motivation see the explanation in #41. In the relational operator case in the equality check for fomulas, we start by deciding if the argument types are the same and then proceed with a homogeneous equality check of the relational operator and the terms https://github.com/katamaran-project/katamaran/blob/26a30b5b62d98f76aca01c7c06611b3fe0199a6c/theories/Symbolic/Solver.v#L605-L609 We can probably avoid the first equality check by reusing the heterogeneous equality for relops https://github.com/katamaran-project/katamaran/blob/26a30b5b62d98f76aca01c7c06611b3fe0199a6c/theories/Syntax/BinOps.v#L130-L143

Note that this only postpones the checking of the indices. A proper solution might require a heterogeneous equality for symbolic terms, next to the existing homogeneous one.