is `NormalizesTo`/`Projection` split still necessary?

[lcnr]

no longer valid reasons:

• normalizes to only normalizes one step/doesn't support rigid aliases (it now does)
• we stored them separately (we no longer do)

maybe difficulties

• nested obligations in fulfillment context need to be handled specially, w.r.t. obligation cause etc
• rn NormalizesTo cannot directly depend on itself, so propagating nested goals gets a lot more something:tm:
  • recursion depth :thinking_face:
  • proof trees :thinking_face: