show that pair construction commutes with taking the core

I do not remember why Core is a typeclass. I could find exactly one other instance, and that's for STSs:

$ rg "Instance.*\bCore\b"
theories/algebra/cmra.v
182:Instance core' `{PCore A} : Core A := λ x, default x (pcore x).

theories/algebra/sts.v
199:Instance sts_core : Core (car sts) := λ x,

Might be worth just defining core x := default x (pcore x)?