Factor plainly out of main BI interface

The intention is to make the axioms compatible with plainly P r := forall s, P s in linear BIs. This is needed to obtain propositional extensionality.