Complete porting Plainly #103
Description
https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/BI/Plainly.lean is not fully done, which caused some issues in #102
It will be nice to check if we ported the most relevant lemmas and instances of the derived connectives