>>13732300Fancy let for type constructors that let you inject single values in them, in a way that (1) injection is compatible with let, (2) the let is associative, i.e. inner lets can be spliced into a let expression.
(let/inject compatibility 1)
let x = inject v
in f x
==
f v
(let/inject compatibility 2)
let x = E
in inject x
==
E
(let associativity)
let y = (let x = E in f x)
in g y
==
let x = E
let y = f x
in g y