Library iris.bi.bi

From iris.bi Require Export derived_laws derived_laws_later big_op.
From iris.bi Require Export updates internal_eq plainly embedding.
Set Default Proof Using "Type".

Module Import bi.
  Export bi.interface.bi.
  Export bi.derived_laws.bi.
  Export bi.derived_laws_later.bi.
End bi.