Deeply normalize obligations in `BestObligation` folder Built on #139513. This establishes a somewhat rough invariant that the `Obligation`'s predicate is always deeply normalized in the folder; when we construct a new obligation we normalize it. Putting this up for discussion since it does affect some goals. r? lcnr