generalizing an unpacked structure

Stream: general

[Moses Schönfinkel]

I have something like {to_structure := {x := X, y := Y}} in my goal's conclusion. Is it possible to express generalize h : {to_structure := {x := X, y := Y}} = a somehow? (This particular formulation errors with invalid structure instance, identifier expected.)

[Simon Hudon]

You may need to give the name of each structure as generalize h : {foo . to_structure := {bar . x := X, y := Y}} = a

[Moses Schönfinkel]

Oh. Thanks. That's going to be a little painful.