missing API to tell injection that a type has decidable equality

[gares]

https://coq.inria.fr/doc/V8.20.0/refman/proof-engine/vernacular-commands.html#coq:cmd.Register-Scheme

so that injection picks it up

https://coq.inria.fr/doc/V8.20.0/refman/proofs/writing-proofs/reasoning-inductives.html#coq:tacn.injection

Beware that injection yields an equality in a sigma type whenever the injected object has a dependent type P with its two instances in different types (P t1 … tn) and (P u1 … un). If t1 and u1 are the same and have for type an inductive type for which a decidable equality has been declared using Scheme Equality, the use of a sigma type is avoided.

to be called in derive.eqbOK