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.