[feature request] equality induction principle for records

[JasonGross]

I'd like something akin to Scheme Equality or Set Decidable Equality Schemes that can generate equality induction principles for records (or for non-recursive inductives, or perhaps for all inductives without indices, like eq_sigT_rect:
https://github.com/coq/coq/blob/3e0334dd48b5d0b03046d0aff1a82867dc98d656/theories/Init/Specif.v#L285-L291

These induction principles are systematic, and go roughly via the encode-decode style of HoTT. If these principles are registered in a table, then inversion_sigma can be generalized
https://github.com/coq/coq/blob/3e0334dd48b5d0b03046d0aff1a82867dc98d656/theories/Init/Tactics.v#L247-L308

cc @herbelin