Dep_elim database not used?

[rnrand]

Was this unfolding database meant to be used in simplify_dep_elim? Because it doesn't seem to be used anywhere in this file, which is a shame. I keep having to call autounfold with dep_elim; simpl_eqs (or simplify_eqs/simplify_dep_elim) in order to get any mileage out of these tactics (eq_rect_r comes up in even the simplest of instances). Would there be a cost to including it in the tactics?

https://github.com/coq/coq/blob/110921a449fcb830ec2a1cd07e3acc32319feae6/theories/Program/Equality.v#L309-L315

[Alizter]

It's more than likely it was omitted. cc @coq/stdlib-maintainers