let-lifting reduction

[JasonGross]

[...] it is certainly worth clarifying when zeta is supposed to be applied. For instance, what is supposed to be the weak reduction of (let _ := y z in fun x => x) 0 in cbv: to block on y in the absence of zeta but to return 0 in the presence of zeta?

Originally posted by @herbelin in #17503 (comment)

Somewhat related to the above comment, and while the devs are discussing reductions, I would like a reduction that neither blocks on let binders nor inlines them, that is one that reduces (let _ := y z in fun x => x) 0 to let _ := y z in 0. I've been calling this "let lifting"; is there a standard name for this transformation during reduction?