Library iris.base_logic.base_logic

From iris.bi Require Export bi.
From iris.base_logic Require Export derived proofmode algebra.
From iris.prelude Require Import options.

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