Implied bounds from normalized ty

[kirloo]

What does this PR do?

Resolves #437

Blocked by #412

How does it work, what questions do you have?

I reused some logic from prove_normalize to retrieve an associated type before feeding it back into the same judgment functions.

AI disclosure

• I used an AI tool for research, autocomplete, or in other minimal ways

[rustbot]

Thanks for contributing to formality! :)
A reviewer will take a look at your PR within a week or two. If not, come talk to us on https://rust-lang.zulipchat.com/#narrow/channel/402470-t-types.2Fformality

[rustbot]

☔ The latest upstream changes (possibly #431) made this pull request unmergeable. Please resolve the merge conflicts.