Library iris.base_logic.base_logic

From iris.bi Require Export bi.
From iris.base_logic Require Export derived proofmode.
Set Default Proof Using "Type".

Module Import uPred.
  Export base_logic.bi.uPred.
  Export derived.uPred.
  Export bi.bi.
End uPred.