custom let that registers for reduction in simp

Stream: mathlib4

[Matthew Ballard]

Given the changes to simp in core, we do want something like letR (WIP) that registers it for use in simp?

[Yaël Dillies]

(I fell off my chair answering this proposal, maybe a sign it would be a disrupting change) Would it be practically different from letI?