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

katamaran/theories/Symbolic/Solver.v

Lines 605 to 609 in 26a30b5

	formula_eqb (@formula_relop _ σ op1 t11 t12) (@formula_relop _ τ op2 t21 t22) with eq_dec σ τ => {
	formula_eqb (@formula_relop _ σ op1 t11 t12) (@formula_relop _ ?(σ) op2 t21 t22) (left eq_refl) :=
	(if eq_dec op1 op2 then true else false) &&& Term_eqb t11 t21 &&& Term_eqb t12 t22;
	formula_eqb (@formula_relop _ σ op1 t11 t12) (@formula_relop _ τ op2 t21 t22) (right _) := false
	};

We can probably avoid the first equality check by reusing the heterogeneous equality for relops

katamaran/theories/Syntax/BinOps.v

Lines 130 to 143 in 26a30b5

	Definition reloptel_eq_dec {σ τ : Ty} (op1 : RelOp σ) (op2 : RelOp τ) :
	dec_eq (A := RelOpTel) (σ,op1) (τ,op2).
	Proof.
	pose (@noConfusion_inv RelOpTel (NoConfusionPackage_RelOp)) as ninv.
	destruct op1, op2;
	try refine (left eq_refl);
	try refine (right (ninv _ _)).
	refine (f_equal_dec (fun ρ => (ρ, eq)) (ninv _ _) (eq_dec σ σ0)).
	refine (f_equal_dec (fun ρ => (ρ, neq)) (ninv _ _) (eq_dec σ σ0)).
	refine (f_equal_dec (fun n => (bvec n, bvsle)) (ninv _ _) (eq_dec n n0)).
	refine (f_equal_dec (fun n => (bvec n, bvslt)) (ninv _ _) (eq_dec n n0)).
	refine (f_equal_dec (fun n => (bvec n, bvule)) (ninv _ _) (eq_dec n n0)).
	refine (f_equal_dec (fun n => (bvec n, bvult)) (ninv _ _) (eq_dec n n0)).
	Defined.

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.