Add Plain instance for bupd

This MR adds a Plain instance for |==> P when P is plain.

In order to be consistent with the naming of other such instances this instance should have the name bupd_plain. However, bupd_plain is already a lemma. I have hence renamed the existing bupd_plain into bupd_elim, which is a better name anyway as it is consistent with intuitionistically_elim, affinely_elim, and plainly_elim.