Better binoptel_eq_dec implementation for update_vector_subrange

[capt-hb]

The current implementation in binoptel_eq_dec for update_vector_subrange is not great:

katamaran/theories/Syntax/BinOps.v

Lines 227 to 233 in fce230f

	| @update_vector_subrange n1 s1 l1 p1, @update_vector_subrange n2 s2 l2 p2 =>
	update_vector_subrange_eq_dec n1 n2 s1 s2 l1 l2 p1 p2
	(* f_equal3_dec
	(fun n s l =>
	((bvec n, bvec l, bvec n), @update_vector_subrange n s l _))
	(ninv ((bvec n1, bvec l1, bvec n1), @update_vector_subrange n1 s1 l1 p1) ((bvec n2, bvec l2, bvec n2), @update_vector_subrange n2 s2 l2 p2))
	(eq_dec n1 n2) (eq_dec s1 s2) (eq_dec l1 l2) *)

With the following implementation for the helper function (using equations):

katamaran/theories/Syntax/BinOps.v

Lines 165 to 172 in fce230f

	#[derive(equations=no)] Equations update_vector_subrange_eq_dec (n1 n2 s1 s2 l1 l2 : nat) (p1 : IsTrue (s1 + l1 <=? n1)) (p2 : IsTrue (s2 + l2 <=? n2)) :
	dec_eq (A := BinOpTel) ((bvec n1, bvec l1, bvec n1),update_vector_subrange s1 l1) ((bvec n2, bvec l2, bvec n2),update_vector_subrange s2 l2) :=
	| n1 | n2 | s1 | s2 | l1 | l2 | p1 | p2 with eq_dec n1 n2, eq_dec s1 s2, eq_dec l1 l2 => {
	| left _ | left _ | left _ => left _
	| right _ | _ | _ => right _
	| _ | right _ | _ => right _
	| _ | _ | right _ => right _
	}.

Ideally, I'd like to use the f_equal3_dec function (defined in theories/Prelude.v), but can't seem to get it to work (see commented code in the first code snippet). After spending some time trying to debug it, I implemented the solution above.