vs doesn't use FUpd
Is there a reason that the definition of vs
explicitly mentions iProp
? In practice it means that its notation can not be used in lifted logics such as monPred
. For example, writing P ==> Q
works at iProp
, but doesn't work at monPred x (iProp _)
even though all of the other notation (that are conceptually very simple) do work at monPred
.