Library iris.bi.bi

From iris.bi Require Export derived_laws_bi derived_laws_sbi
     big_op updates plainly embedding.
Set Default Proof Using "Type".

Module Import bi.
  Export bi.interface.bi.
  Export bi.derived_laws_bi.bi.
  Export bi.derived_laws_sbi.bi.
End bi.