normalise subtype.val and coe

Stream: general

[Johan Commelin]

I have an expression with a whole bunch of x.val and \u x occuring. I want to kill the thing with ring. However, ring gets stuck because those terms are not syntactically equal, even if they are defeq. I can of course change to a normalised expression, but I'd rather just rw the coercions (or the .vals) away. Can this be done currently?

[Kenny Lau]

just make a simp lemma

[Johan Commelin]

Aaah! There is unfold_coes.