ext and with_top/bot

Stream: general

[Yury G. Kudryashov]

Sometimes ext applies a lemma for another type because it can see through type synonyms. While this is sometimes useful (e.g., if you're proving an ext lemma for a type synonym using the ext lemma for the original type), quite often this is not what I want. For me, the most annoying scenario is ext applying docs#option.ext to equality of two docs#ennreal numbers (so I have to use ext1 to prove equality of measures).
It would be nice to stop ext seeing through these definitions. The old behavior can be available through ext! or ext { some_option := tt }.