diff --git a/_CoqProject b/_CoqProject
index b231baee4692d91ae15f55eb18138163caac494a..17a6dd76a953d079a8a05d1807154c5b03257346 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -56,6 +56,7 @@ iris/algebra/lib/mono_nat.v
 iris/algebra/lib/gset_bij.v
 iris/si_logic/siprop.v
 iris/si_logic/bi.v
+iris/si_logic/algebra.v
 iris/bi/notation.v
 iris/bi/interface.v
 iris/bi/derived_connectives.v
diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 138969cfca5b87a2767ffbb2149a2e74a0a630c0..6e254b5aa41f41542df3bce5ff4c994fc42a95d5 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -1,65 +1,68 @@
 From iris.algebra Require Import cmra view auth agree csum list excl gmap.
 From iris.algebra.lib Require Import excl_auth gmap_view.
-From iris.base_logic Require Import bi derived.
+From iris.si_logic Require Import algebra.
+From iris.base_logic Require Import cmra_valid.
 From iris.prelude Require Import options.
 
 (** Internalized properties of our CMRA constructions. *)
-Local Coercion uPred_holds : uPred >-> Funclass.
+Local Coercion siProp_holds : siProp >-> Funclass.
 
-Section upred.
-Context {M : ucmra}.
+Section bi_cmra_valid.
+Context {PROP : bi} `{!BiEmbed siPropI PROP}.
 
 (* Force implicit argument M *)
-Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
-Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+Notation "P ⊢ Q" := (bi_entails (PROP:=PROP) P Q).
+Notation "P ⊣⊢ Q" := (equiv (A:=PROP) P%I Q%I).
+
+Local Definition unseal_eqs :=
+  (@embed_emp, @embed_pure,
+    @embed_and, @embed_or, @embed_impl, @embed_forall, @embed_exist,
+    @embed_sep, @embed_wand).
+Local Ltac unseal_embed :=
+  bi_cmra_valid.unseal;
+  rewrite -?unseal_eqs;
+  first [apply embed_proper | apply embed_mono | idtac ].
 
 Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-Proof. by uPred.unseal. Qed.
-Lemma option_validI {A : cmra} (mx : option A) :
-  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
-Proof. uPred.unseal. by destruct mx. Qed.
+Proof. unseal_embed. exact: siProp_algebra.prod_validI. Qed.
+Lemma option_validI `{!BiEmbedEmp siPropI PROP} {A : cmra} (mx : option A) :
+  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => emp end.
+Proof. destruct mx; unseal_embed; exact: siProp_algebra.option_validI. Qed.
 Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
   ✓ g ⊣⊢ ∀ i, ✓ g i.
-Proof. by uPred.unseal. Qed.
+Proof. unseal_embed. exact: siProp_algebra.discrete_fun_validI. Qed.
 
 Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1⌝%Qp.
-Proof. rewrite uPred.discrete_valid frac_valid //. Qed.
+Proof. unseal_embed. exact: siProp_algebra.frac_validI. Qed.
 
-Section gmap_ofe.
+(* Section gmap_ofe.
   Context `{Countable K} {A : ofe}.
   Implicit Types m : gmap K A.
   Implicit Types i : K.
 
   Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
   Proof. by uPred.unseal. Qed.
-End gmap_ofe.
+End gmap_ofe. *)
 
 Section gmap_cmra.
   Context `{Countable K} {A : cmra}.
   Implicit Types m : gmap K A.
 
   Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
-  Proof. by uPred.unseal. Qed.
+  Proof. unseal_embed. exact: siProp_algebra.gmap_validI. Qed.
   Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢ ✓ x.
-  Proof.
-    rewrite gmap_validI. apply: anti_symm.
-    - rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
-    - apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
-      + rewrite lookup_singleton option_validI. done.
-      + rewrite lookup_singleton_ne // option_validI.
-        apply bi.True_intro.
-  Qed.
+  Proof. unseal_embed. exact: siProp_algebra.singleton_validI. Qed.
 End gmap_cmra.
 
-Section list_ofe.
+(* Section list_ofe.
   Context {A : ofe}.
   Implicit Types l : list A.
 
   Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
   Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
-End list_ofe.
+End list_ofe. *)
 
-Section excl.
+(* Section excl.
   Context {A : ofe}.
   Implicit Types a b : A.
   Implicit Types x y : excl A.
@@ -78,9 +81,9 @@ Section excl.
   Lemma excl_validI x :
     ✓ x ⊣⊢ if x is ExclBot then False else True.
   Proof. uPred.unseal. by destruct x. Qed.
-End excl.
+End excl. *)
 
-Section agree.
+(* Section agree.
   Context {A : ofe}.
   Implicit Types a b : A.
   Implicit Types x y : agree A.
@@ -114,7 +117,7 @@ Section csum_ofe.
     uPred.unseal; do 2 split; first by destruct 1.
       by destruct x, y; try destruct 1; try constructor.
   Qed.
-End csum_ofe.
+End csum_ofe. *)
 
 Section csum_cmra.
   Context {A B : cmra}.
@@ -127,7 +130,7 @@ Section csum_cmra.
                       | Cinr b => ✓ b
                       | CsumBot => False
                       end.
-  Proof. uPred.unseal. by destruct x. Qed.
+  Proof. destruct x; unseal_embed; exact: siProp_algebra.csum_validI. Qed.
 End csum_cmra.
 
 Section view.
@@ -137,62 +140,45 @@ Section view.
   Implicit Types b : B.
   Implicit Types x y : view rel.
 
-  Lemma view_both_dfrac_validI_1 (relI : uPred M) dq a b :
-    (∀ n (x : M), rel n a b → relI n x) →
-    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ relI.
-  Proof.
-    intros Hrel. uPred.unseal. split=> n x _ /=.
-    rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
-  Qed.
-  Lemma view_both_dfrac_validI_2 (relI : uPred M) dq a b :
-    (∀ n (x : M), relI n x → rel n a b) →
-    ⌜✓dq⌝ ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
-  Proof.
-    intros Hrel. uPred.unseal. split=> n x _ /=.
-    rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
-  Qed.
-  Lemma view_both_dfrac_validI (relI : uPred M) dq a b :
-    (∀ n (x : M), rel n a b ↔ relI n x) →
-    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
-  Proof.
-    intros. apply (anti_symm _);
-      [apply view_both_dfrac_validI_1|apply view_both_dfrac_validI_2]; naive_solver.
-  Qed.
-
-  Lemma view_both_validI_1 (relI : uPred M) a b :
-    (∀ n (x : M), rel n a b → relI n x) →
-    ✓ (●V a ⋅ ◯V b : view rel) ⊢ relI.
-  Proof. intros. by rewrite view_both_dfrac_validI_1 // bi.and_elim_r. Qed.
-  Lemma view_both_validI_2 (relI : uPred M) a b :
-    (∀ n (x : M), relI n x → rel n a b) →
-    relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
-  Proof.
-    intros. rewrite -view_both_dfrac_validI_2 //.
-    apply bi.and_intro; [|done]. by apply bi.pure_intro.
-  Qed.
-  Lemma view_both_validI (relI : uPred M) a b :
-    (∀ n (x : M), rel n a b ↔ relI n x) →
-    ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ relI.
-  Proof.
-    intros. apply (anti_symm _);
-      [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
-  Qed.
-
-  Lemma view_auth_dfrac_validI (relI : uPred M) dq a :
-    (∀ n (x : M), relI n x ↔ rel n a ε) →
-    ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
-  Proof.
-    intros. rewrite -(right_id ε op (●V{dq} a)). by apply view_both_dfrac_validI.
-  Qed.
-  Lemma view_auth_validI (relI : uPred M) a :
-    (∀ n (x : M), relI n x ↔ rel n a ε) →
-    ✓ (●V a : view rel) ⊣⊢ relI.
-  Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.
-
-  Lemma view_frag_validI (relI : uPred M) b :
-    (∀ n (x : M), relI n x ↔ ∃ a, rel n a b) →
-    ✓ (◯V b : view rel) ⊣⊢ relI.
-  Proof. uPred.unseal=> Hrel. split=> n x _. by rewrite Hrel. Qed.
+  Lemma view_both_dfrac_validI_1 (relI : siProp) dq a b :
+    (∀ n, rel n a b → relI n) →
+    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ ⎡ relI ⎤.
+  Proof. intros. unseal_embed. exact: siProp_algebra.view_both_dfrac_validI_1. Qed.
+  Lemma view_both_dfrac_validI_2 (relI : siProp) dq a b :
+    (∀ n, relI n → rel n a b) →
+    ⌜✓dq⌝ ∧ ⎡ relI ⎤ ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
+  Proof. intros. unseal_embed. exact: siProp_algebra.view_both_dfrac_validI_2. Qed.
+  Lemma view_both_dfrac_validI (relI : siProp) dq a b :
+    (∀ n, rel n a b ↔ relI n) →
+    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ ⎡ relI ⎤.
+  Proof. intros. unseal_embed. exact: siProp_algebra.view_both_dfrac_validI. Qed.
+
+  Lemma view_both_validI_1 (relI : siProp) a b :
+    (∀ n, rel n a b → relI n) →
+    ✓ (●V a ⋅ ◯V b : view rel) ⊢ ⎡ relI ⎤.
+  Proof. intros. unseal_embed. exact: siProp_algebra.view_both_validI_1. Qed.
+  Lemma view_both_validI_2 (relI : siProp) a b :
+    (∀ n, relI n → rel n a b) →
+    ⎡ relI ⎤ ⊢ ✓ (●V a ⋅ ◯V b : view rel).
+  Proof. intros. unseal_embed. exact: siProp_algebra.view_both_validI_2. Qed.
+  Lemma view_both_validI (relI : siProp) a b :
+    (∀ n, rel n a b ↔ relI n) →
+    ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ ⎡ relI ⎤.
+  Proof. intros. unseal_embed. exact: siProp_algebra.view_both_validI. Qed.
+
+  Lemma view_auth_dfrac_validI (relI : siProp) dq a :
+    (∀ n, relI n ↔ rel n a ε) →
+    ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ ⎡ relI ⎤.
+  Proof. intros. unseal_embed. exact: siProp_algebra.view_auth_dfrac_validI. Qed.
+  Lemma view_auth_validI (relI : siProp) a :
+    (∀ n, relI n ↔ rel n a ε) →
+    ✓ (●V a : view rel) ⊣⊢ ⎡ relI ⎤.
+  Proof. intros. unseal_embed. exact: siProp_algebra.view_auth_validI. Qed.
+
+  Lemma view_frag_validI (relI : siProp) b :
+    (∀ n, relI n ↔ ∃ a, rel n a b) →
+    ✓ (◯V b : view rel) ⊣⊢ ⎡ relI ⎤.
+  Proof. intros. unseal_embed. exact: siProp_algebra.view_frag_validI. Qed.
 End view.
 
 Section auth.
@@ -201,33 +187,25 @@ Section auth.
   Implicit Types x y : auth A.
 
   Lemma auth_auth_dfrac_validI dq a : ✓ (●{dq} a) ⊣⊢ ⌜✓dq⌝ ∧ ✓ a.
-  Proof.
-    apply view_auth_dfrac_validI=> n. uPred.unseal; split; [|by intros [??]].
-    split; [|done]. apply ucmra_unit_leastN.
-  Qed.
+  Proof. unseal_embed. exact: siProp_algebra.auth_auth_dfrac_validI. Qed.
   Lemma auth_auth_validI a : ✓ (● a) ⊣⊢ ✓ a.
-  Proof.
-    by rewrite auth_auth_dfrac_validI bi.pure_True // left_id.
-  Qed.
+  Proof. unseal_embed. exact: siProp_algebra.auth_auth_validI. Qed.
 
   Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
-  Proof.
-    apply view_frag_validI=> n x.
-    rewrite auth_view_rel_exists. by uPred.unseal.
-  Qed.
+  Proof. unseal_embed. exact: siProp_algebra.auth_frag_validI. Qed.
 
-  Lemma auth_both_dfrac_validI dq a b :
+  (* Lemma auth_both_dfrac_validI dq a b :
     ✓ (●{dq} a ⋅ ◯ b) ⊣⊢ ⌜✓dq⌝ ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
   Proof. apply view_both_dfrac_validI=> n. by uPred.unseal. Qed.
   Lemma auth_both_validI a b :
     ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
   Proof.
     by rewrite auth_both_dfrac_validI bi.pure_True // left_id.
-  Qed.
+  Qed. *)
 
 End auth.
 
-Section excl_auth.
+(* Section excl_auth.
   Context {A : ofe}.
   Implicit Types a b : A.
 
@@ -237,9 +215,9 @@ Section excl_auth.
     apply bi.exist_elim=> -[[c|]|];
       by rewrite option_equivI /= excl_equivI //= bi.False_elim.
   Qed.
-End excl_auth.
+End excl_auth. *)
 
-Section gmap_view.
+(* Section gmap_view.
   Context {K : Type} `{Countable K} {V : ofe}.
   Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
 
@@ -260,6 +238,6 @@ Section gmap_view.
     rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
   Qed.
 
-End gmap_view.
+End gmap_view. *)
 
-End upred.
+End bi_cmra_valid.
diff --git a/iris/base_logic/cmra_valid.v b/iris/base_logic/cmra_valid.v
index 6c973eb3ec040de69334e423beef27ea28800843..01335f9a4e9118b9ca8b8e8c5f7e5a1a3474dcbd 100644
--- a/iris/base_logic/cmra_valid.v
+++ b/iris/base_logic/cmra_valid.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import cmra.
-From iris.si_logic Require Export bi siprop.
+From iris.si_logic Require Export bi.
 From iris.prelude Require Import options.
 
 Definition bi_cmra_valid_def
@@ -16,7 +16,7 @@ Notation "✓ x" := (bi_cmra_valid x) (at level 20) : bi_scope.
 
 Module bi_cmra_valid.
 Ltac unseal :=
-  rewrite !bi_cmra_valid_eq /=.
+  rewrite !bi_cmra_valid_eq /bi_cmra_valid_def /=.
 End bi_cmra_valid.
 
 Section valid_props.
@@ -27,7 +27,7 @@ Import bi_cmra_valid.
 
 Global Instance cmra_valid_ne :
   NonExpansive (@bi_cmra_valid _ _ A).
-Proof. unseal => ????. by apply embed_ne, siProp_primitive.cmra_valid_ne. Qed.
+Proof. unseal => ????. by apply embed_ne, siProp.cmra_valid_ne. Qed.
 
 Global Instance cmra_valid_proper :
   Proper ((≡) ==> (⊣⊢)) (@bi_cmra_valid _ _ A) := ne_proper _.
@@ -35,20 +35,19 @@ Global Instance cmra_valid_proper :
 Lemma cmra_valid_intro P a : ✓ a → P ⊢ (✓ a).
 Proof.
   unseal => Ha.
-  rewrite /bi_cmra_valid_def -(siProp_primitive.cmra_valid_intro True%I) //.
-  rewrite embed_pure. apply bi.True_intro.
+  rewrite -(siProp.cmra_valid_intro True%I) // embed_pure. apply bi.True_intro.
 Qed.
 Lemma cmra_valid_elim (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
 Proof.
-  unseal=> ?. by rewrite /bi_cmra_valid_def siProp_primitive.cmra_valid_elim // embed_pure.
+  unseal=> ?. by rewrite siProp.cmra_valid_elim // embed_pure.
 Qed.
 
 Lemma cmra_valid_weaken (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
-Proof. unseal. apply embed_mono, siProp_primitive.cmra_valid_weaken. Qed.
+Proof. unseal. apply embed_mono, siProp.cmra_valid_weaken. Qed.
 
 Lemma discrete_valid `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
 Proof.
-  unseal. by rewrite /bi_cmra_valid_def siProp_primitive.discrete_valid embed_pure.
+  unseal. by rewrite siProp.discrete_valid embed_pure.
 Qed.
 
 Lemma valid_entails {B : cmra} (a : A) (b : B) :
diff --git a/iris/si_logic/algebra.v b/iris/si_logic/algebra.v
new file mode 100644
index 0000000000000000000000000000000000000000..349945117be967a67ff0d4ccec6ac30639bb0c8c
--- /dev/null
+++ b/iris/si_logic/algebra.v
@@ -0,0 +1,267 @@
+From iris.algebra Require Import cmra view auth agree csum list excl gmap.
+From iris.algebra.lib Require Import excl_auth gmap_view.
+From iris.si_logic Require Import bi.
+From iris.prelude Require Import options.
+
+(** Internalized properties of our CMRA constructions. *)
+Local Coercion siProp_holds : siProp >-> Funclass.
+
+Module siProp_algebra.
+Section siprop.
+
+Notation "P ⊢ Q" := (bi_entails (PROP:=siPropI) P%I Q%I).
+Notation "P ⊣⊢ Q" := (equiv (A:=siPropI) P%I Q%I).
+Notation "✓ x" := (siProp_cmra_valid x) : bi_scope.
+
+Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
+Proof. by siProp.unseal. Qed.
+Lemma option_validI {A : cmra} (mx : option A) :
+  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
+Proof. siProp.unseal. by destruct mx. Qed.
+Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
+  ✓ g ⊣⊢ ∀ i, ✓ g i.
+Proof. by siProp.unseal. Qed.
+
+Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1⌝%Qp.
+Proof. rewrite siProp.discrete_valid frac_valid //. Qed.
+
+Section gmap_ofe.
+  Context `{Countable K} {A : ofe}.
+  Implicit Types m : gmap K A.
+  Implicit Types i : K.
+
+  Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
+  Proof. by siProp.unseal. Qed.
+End gmap_ofe.
+
+Section gmap_cmra.
+  Context `{Countable K} {A : cmra}.
+  Implicit Types m : gmap K A.
+
+  Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
+  Proof. by siProp.unseal. Qed.
+  Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢ ✓ x.
+  Proof.
+    rewrite gmap_validI. apply: anti_symm.
+    - rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
+    - apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
+      + rewrite lookup_singleton option_validI. done.
+      + rewrite lookup_singleton_ne // option_validI.
+        apply bi.True_intro.
+  Qed.
+End gmap_cmra.
+
+Section list_ofe.
+  Context {A : ofe}.
+  Implicit Types l : list A.
+
+  Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
+  Proof. siProp.unseal; constructor=> n. apply list_dist_lookup. Qed.
+End list_ofe.
+
+Section excl.
+  Context {A : ofe}.
+  Implicit Types a b : A.
+  Implicit Types x y : excl A.
+
+  Lemma excl_equivI x y :
+    x ≡ y ⊣⊢ match x, y with
+                        | Excl a, Excl b => a ≡ b
+                        | ExclBot, ExclBot => True
+                        | _, _ => False
+                        end.
+  Proof.
+    siProp.unseal. do 2 split.
+    - by destruct 1.
+    - by destruct x, y; try constructor.
+  Qed.
+  Lemma excl_validI x :
+    ✓ x ⊣⊢ if x is ExclBot then False else True.
+  Proof. siProp.unseal. by destruct x. Qed.
+End excl.
+
+Section agree.
+  Context {A : ofe}.
+  Implicit Types a b : A.
+  Implicit Types x y : agree A.
+
+  Lemma agree_equivI a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b).
+  Proof.
+    siProp.unseal. do 2 split.
+    - intros Hx. exact: (inj to_agree).
+    - intros Hx. exact: to_agree_ne.
+  Qed.
+  Lemma agree_validI x y : ✓ (x ⋅ y) ⊢ x ≡ y.
+  Proof. siProp.unseal; split=> r n ; by apply: agree_op_invN. Qed.
+
+  Lemma to_agree_uninjI x : ✓ x ⊢ ∃ a, to_agree a ≡ x.
+  Proof. siProp.unseal. split=> n. exact: to_agree_uninjN. Qed.
+End agree.
+
+Section csum_ofe.
+  Context {A B : ofe}.
+  Implicit Types a : A.
+  Implicit Types b : B.
+
+  Lemma csum_equivI (x y : csum A B) :
+    x ≡ y ⊣⊢ match x, y with
+                        | Cinl a, Cinl a' => a ≡ a'
+                        | Cinr b, Cinr b' => b ≡ b'
+                        | CsumBot, CsumBot => True
+                        | _, _ => False
+                        end.
+  Proof.
+    siProp.unseal; do 2 split; first by destruct 1.
+      by destruct x, y; try destruct 1; try constructor.
+  Qed.
+End csum_ofe.
+
+Section csum_cmra.
+  Context {A B : cmra}.
+  Implicit Types a : A.
+  Implicit Types b : B.
+
+  Lemma csum_validI (x : csum A B) :
+    ✓ x ⊣⊢ match x with
+                      | Cinl a => ✓ a
+                      | Cinr b => ✓ b
+                      | CsumBot => False
+                      end.
+  Proof. siProp.unseal. by destruct x. Qed.
+End csum_cmra.
+
+Section view.
+  Context {A B} (rel : view_rel A B).
+  Implicit Types a : A.
+  Implicit Types ag : option (frac * agree A).
+  Implicit Types b : B.
+  Implicit Types x y : view rel.
+  Local Arguments siProp_holds !_ _ /.
+
+  Lemma view_both_dfrac_validI_1 (relI : siProp) dq a b :
+    (∀ n, rel n a b → relI n) →
+    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ relI.
+  Proof.
+    intros Hrel. siProp.unseal. split=> n /=.
+    rewrite /= view_both_dfrac_validN. by move=> [? /Hrel].
+  Qed.
+  Lemma view_both_dfrac_validI_2 (relI : siProp) dq a b :
+    (∀ n, relI n → rel n a b) →
+    ⌜✓dq⌝ ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
+  Proof.
+    intros Hrel. siProp.unseal. split=> n /=.
+    rewrite /= view_both_dfrac_validN. by move=> [? /Hrel].
+  Qed.
+  Lemma view_both_dfrac_validI (relI : siProp) dq a b :
+    (∀ n, rel n a b ↔ relI n) →
+    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
+  Proof.
+    intros. apply (anti_symm _);
+      [apply view_both_dfrac_validI_1|apply view_both_dfrac_validI_2]; naive_solver.
+  Qed.
+
+  Lemma view_both_validI_1 (relI : siProp) a b :
+    (∀ n, rel n a b → relI n) →
+    ✓ (●V a ⋅ ◯V b : view rel) ⊢ relI.
+  Proof. intros. by rewrite view_both_dfrac_validI_1 // bi.and_elim_r. Qed.
+  Lemma view_both_validI_2 (relI : siProp) a b :
+    (∀ n, relI n → rel n a b) →
+    relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
+  Proof.
+    intros. rewrite -view_both_dfrac_validI_2 //.
+    apply bi.and_intro; [|done]. by apply bi.pure_intro.
+  Qed.
+  Lemma view_both_validI (relI : siProp) a b :
+    (∀ n, rel n a b ↔ relI n) →
+    ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ relI.
+  Proof.
+    intros. apply (anti_symm _);
+      [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
+  Qed.
+
+  Lemma view_auth_dfrac_validI (relI : siProp) dq a :
+    (∀ n, relI n ↔ rel n a ε) →
+    ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
+  Proof.
+    intros. rewrite -(right_id ε op (●V{dq} a)). by apply view_both_dfrac_validI.
+  Qed.
+  Lemma view_auth_validI (relI : siProp) a :
+    (∀ n, relI n ↔ rel n a ε) →
+    ✓ (●V a : view rel) ⊣⊢ relI.
+  Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.
+
+  Lemma view_frag_validI (relI : siProp) b :
+    (∀ n, relI n ↔ ∃ a, rel n a b) →
+    ✓ (◯V b : view rel) ⊣⊢ relI.
+  Proof. siProp.unseal=> Hrel. split=> n. by rewrite Hrel. Qed.
+End view.
+
+Section auth.
+  Context {A : ucmra}.
+  Implicit Types a b : A.
+  Implicit Types x y : auth A.
+
+  Lemma auth_auth_dfrac_validI dq a : ✓ (●{dq} a) ⊣⊢ ⌜✓dq⌝ ∧ ✓ a.
+  Proof.
+    apply view_auth_dfrac_validI=> n. siProp.unseal; split; [|by intros [??]].
+    split; [|done]. apply ucmra_unit_leastN.
+  Qed.
+  Lemma auth_auth_validI a : ✓ (● a) ⊣⊢ ✓ a.
+  Proof.
+    by rewrite auth_auth_dfrac_validI bi.pure_True // left_id.
+  Qed.
+
+  Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
+  Proof.
+    apply view_frag_validI=> n.
+    rewrite auth_view_rel_exists. by siProp.unseal.
+  Qed.
+
+  Lemma auth_both_dfrac_validI dq a b :
+    ✓ (●{dq} a ⋅ ◯ b) ⊣⊢ ⌜✓dq⌝ ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+  Proof. apply view_both_dfrac_validI=> n. by siProp.unseal. Qed.
+  Lemma auth_both_validI a b :
+    ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+  Proof.
+    by rewrite auth_both_dfrac_validI bi.pure_True // left_id.
+  Qed.
+
+End auth.
+
+Section excl_auth.
+  Context {A : ofe}.
+  Implicit Types a b : A.
+
+  Lemma excl_auth_agreeI a b : ✓ (●E a ⋅ ◯E b) ⊢ (a ≡ b).
+  Proof.
+    rewrite auth_both_validI bi.and_elim_l.
+    apply bi.exist_elim=> -[[c|]|];
+      by rewrite option_equivI /= excl_equivI //= bi.False_elim.
+  Qed.
+End excl_auth.
+
+Section gmap_view.
+  Context {K : Type} `{Countable K} {V : ofe}.
+  Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
+
+  Lemma gmap_view_both_validI m k dq v :
+    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ⊢
+    ✓ dq ∧ m !! k ≡ Some v.
+  Proof.
+    rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
+    intros n. siProp.unseal. apply gmap_view.gmap_view_rel_lookup.
+  Qed.
+
+  Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
+    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢
+    ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
+  Proof.
+    rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI=> n.
+    rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
+    rewrite -pair_op pair_validN to_agree_op_validN. by siProp.unseal.
+  Qed.
+
+End gmap_view.
+
+End siprop.
+End siProp_algebra.
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index 40464d70f27e231cc6845320256fd38f6518a863..2a04dd21ad19744d3a344fbd44816ba0ff87da09 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -177,6 +177,26 @@ Proof. done. Qed.
 
 Module siProp.
 Section restate.
+
+(** Valid *)
+Notation "✓ x" := (siProp_cmra_valid x) : bi_scope.
+
+Global Instance cmra_valid_ne {A : cmra} :
+  NonExpansive (@siProp_cmra_valid A) := siProp_primitive.cmra_valid_ne.
+Global Instance cmra_valid_proper {A : cmra} :
+  Proper ((≡) ==> (⊣⊢)) (@siProp_cmra_valid A) := ne_proper _.
+
+Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ ✓ a.
+Proof. exact: siProp_primitive.cmra_valid_intro. Qed.
+Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+Proof. exact: siProp_primitive.cmra_valid_elim. Qed.
+Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Proof. exact: siProp_primitive.cmra_valid_weaken. Qed.
+
+Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+Proof. exact: siProp_primitive.discrete_valid. Qed.
+
+(** Soundness *)
 Lemma pure_soundness φ : (⊢@{siPropI} ⌜ φ ⌝) → φ.
 Proof. apply pure_soundness. Qed.
 
@@ -186,4 +206,15 @@ Proof. apply internal_eq_soundness. Qed.
 Lemma later_soundness (P : siProp) : (⊢ ▷ P) → ⊢ P.
 Proof. apply later_soundness. Qed.
 End restate.
+
+(** New unseal tactic that also unfolds the BI layer.
+    TODO: Can we get rid of this? *)
+    Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
+    unfold bi_emp; simpl;
+    unfold siProp_emp, bupd, bi_bupd_bupd, bi_pure,
+      bi_and, bi_or, bi_impl, bi_forall, bi_exist,
+      bi_sep, bi_wand, bi_persistently, bi_later; simpl;
+    unfold internal_eq, bi_internal_eq_internal_eq,
+      plainly, bi_plainly_plainly; simpl;
+    siProp_primitive.unseal.
 End siProp.