attribute [ext] subsingleton.elim

Stream: general

[Scott Morrison]

I noticed that ext isn't blasting through equalities of subsingletons, and was going to begin trying out attribute [ext] subsingleton.elim, but immediately got an error message:
only constants and Pi types are supported: α

[Scott Morrison]

Any ideas?

[Mario Carneiro]

We could use subsingleton.elim as the fallback if the type is not a constant?

[Mario Carneiro]

or you could use congr instead of ext since it's already hooked up to do this