The plausibly modality
Much of this is based on https://gitlab.mpisws.org/FP/iriscoq/merge_requests/184#note_31510 by @amintimany, but made to work for nonaffine BIs and changed in such a way that it follows the Iris naming conventions.
Some TODOs:
 Should the modality be affine or absorbing?

Could we change the definition so that the following result holds even if
P
is not absorbing:Lemma plain_plausibly P `{!Plain P, !Absorbing P} : <plausible> P ⊣⊢ P.

The properties that the modality commutes with
▷
and∀
are pretty useless because they only hold when the proposition inside is plain (they thus trivially follow fromplain_plausibly
). Do we have such lemmas in general for some connectives? Otherwise, I propose to remove these lemmas.  It would be useful to have some proof mode instances to support easy reasoning using the modality. @amintimany has some in his post, but what we had is not complete.
cc @jtassaro