Commit 2026-04-29 09:12 b51f26d7

chore(GRewrite): copy how rw elaborates (#38558) Since grw has been merged, some subtle changes have been made to how rw elaborates. This PR copies those changes over to grw. In one place, a proof had to be adapted. Previously, the side goals created by grw were filled in by unification in the next rewrite. This is not possible anymore because these side goals are now marked synthetic opaque.