Library iris.algebra.base

From Coq.ssr Require Export ssreflect.
From stdpp Require Export prelude.
Set Default Proof Using "Type".
Global Open Scope general_if_scope.
Global Set SsrOldRewriteGoalsOrder. Ltac done := stdpp.tactics.done.