Improve `coreP` construction.

Some improvements to the bi/lib/core construction:

• Rename coreP_wand into coreP_entails since it does not involve wands.
• Generalize coreP_entails to non-affine BIs.
• Add instance coreP_affine P : Affine P → Affine (coreP P) and lemma coreP_wand P Q : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q.