Packing records?

[mtzguido]

From call today: can we add some syntax like pack {x=e;y=f} as r, that elaborates to something like let r = {x=e; y=f}; rewrite each e as r.x; rewrite f as r.y; to comfortably use records? Or would it be enough to define a packing function for each given type? The latter alternative would not do any rewrite in the frame.