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)?