diff --git a/_CoqProject b/_CoqProject
index 32d0d4755f928e8127675c14ea1fb81b3c82a646..a8bfee56a59573f33339320f1144e1e01373b38e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -70,6 +70,7 @@ theories/base_logic/bi.v
 theories/base_logic/derived.v
 theories/base_logic/proofmode.v
 theories/base_logic/base_logic.v
+theories/base_logic/algebra.v
 theories/base_logic/bupd_alt.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 3fd06e292ee674f2add38e4ee8e373983fd64640..c0ae62c9199d1cdc0f4d30c6c57cc849314e6e86 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -1,7 +1,6 @@
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import list.
-From iris.base_logic Require Import base_logic.
 From iris Require Import options.
+
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
@@ -257,18 +256,6 @@ Qed.
 Lemma to_agree_op_valid_L `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) ↔ a = b.
 Proof. rewrite to_agree_op_valid. by fold_leibniz. Qed.
 
-(** Internalized properties *)
-Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢@{uPredI M} (a ≡ b).
-Proof.
-  uPred.unseal. do 2 split.
-  - intros Hx. exact: (inj to_agree).
-  - intros Hx. exact: to_agree_ne.
-Qed.
-Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢@{uPredI M} x ≡ y.
-Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
-
-Lemma to_agree_uninjI {M} x : ✓ x ⊢@{uPredI M} ∃ a, to_agree a ≡ x.
-Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
 End agree.
 
 Instance: Params (@to_agree) 1 := {}.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index b6ea8744f2f07ea7e6f3371aaafd7e20b96cfc0d..241c20e444e3f97ff656c3992dea10aec966fdae 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -1,6 +1,5 @@
 From iris.algebra Require Export view.
-From iris.algebra Require Import proofmode_classes.
-From iris.base_logic Require Import base_logic.
+From iris.algebra Require Import proofmode_classes big_op.
 From iris Require Import options.
 
 (** The authoritative camera with fractional authoritative elements *)
@@ -239,29 +238,6 @@ Section auth.
     ● a1 ⋅ ◯ b1 ≼ ● a2 ⋅ ◯ b2 ↔ a1 ≡ a2 ∧ b1 ≼ b2.
   Proof. apply view_both_included. Qed.
 
-  (** Internalized properties *)
-  Lemma auth_auth_frac_validI {M} q a : ✓ (●{q} a) ⊣⊢@{uPredI M} ✓ q ∧ ✓ a.
-  Proof.
-    apply view_auth_frac_validI=> n. uPred.unseal; split; [|by intros [??]].
-    split; [|done]. apply ucmra_unit_leastN.
-  Qed.
-  Lemma auth_auth_validI {M} a : ✓ (● a) ⊣⊢@{uPredI M} ✓ a.
-  Proof.
-    by rewrite auth_auth_frac_validI uPred.discrete_valid bi.pure_True // left_id.
-  Qed.
-
-  Lemma auth_frag_validI {M} a : ✓ (◯ a) ⊣⊢@{uPredI M} ✓ a.
-  Proof. apply view_frag_validI. Qed.
-
-  Lemma auth_both_frac_validI {M} q a b :
-    ✓ (●{q} a ⋅ ◯ b) ⊣⊢@{uPredI M} ✓ q ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
-  Proof. apply view_both_frac_validI=> n. by uPred.unseal. Qed.
-  Lemma auth_both_validI {M} a b :
-    ✓ (● a ⋅ ◯ b) ⊣⊢@{uPredI M} (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
-  Proof.
-    by rewrite auth_both_frac_validI uPred.discrete_valid bi.pure_True // left_id.
-  Qed.
-
   (** Updates *)
   Lemma auth_update a b a' b' :
     (a,b) ~l~> (a',b') → ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'.
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 82f46b1a5ac92ee0a4424e795c889dc818f3d988..2089b469b76cadfe2f7eaa1d4f046780eb25f67f 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import local_updates.
-From iris.base_logic Require Import base_logic.
+From iris.algebra Require Import updates local_updates.
 From iris Require Import options.
+
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
 Local Arguments validN _ _ _ !_ /.
@@ -26,7 +26,7 @@ Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
 Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
   match x with Cinr b => Some b | _ => None end.
 
-Section cofe.
+Section ofe.
 Context {A B : ofeT}.
 Implicit Types a : A.
 Implicit Types b : B.
@@ -108,19 +108,7 @@ Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
 Global Instance Cinr_discrete b : Discrete b → Discrete (Cinr b).
 Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
 
-(** Internalized properties *)
-Lemma csum_equivI {M} (x y : csum A B) :
-  x ≡ y ⊣⊢@{uPredI M} match x, y with
-                      | Cinl a, Cinl a' => a ≡ a'
-                      | Cinr b, Cinr b' => b ≡ b'
-                      | CsumBot, CsumBot => True
-                      | _, _ => False
-                      end.
-Proof.
-  uPred.unseal; do 2 split; first by destruct 1.
-  by destruct x, y; try destruct 1; try constructor.
-Qed.
-End cofe.
+End ofe.
 
 Arguments csumO : clear implicits.
 
@@ -321,15 +309,6 @@ Proof.
   - naive_solver by f_equiv.
 Qed.
 
-(** Internalized properties *)
-Lemma csum_validI {M} (x : csum A B) :
-  ✓ x ⊣⊢@{uPredI M} match x with
-                    | Cinl a => ✓ a
-                    | Cinr b => ✓ b
-                    | CsumBot => False
-                    end.
-Proof. uPred.unseal. by destruct x. Qed.
-
 (** Updates *)
 Lemma csum_update_l (a1 a2 : A) : a1 ~~> a2 → Cinl a1 ~~> Cinl a2.
 Proof.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index fcf4f879d34ff9736684b0eaddc5b652f44ed1b8..6fcb9e9bd257463eb7ec7d850bf4f0c9721e9109 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra.
-From iris.base_logic Require Import base_logic.
 From iris Require Import options.
+
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
@@ -94,20 +94,6 @@ Canonical Structure exclR := CmraT (excl A) excl_cmra_mixin.
 Global Instance excl_cmra_discrete : OfeDiscrete A → CmraDiscrete exclR.
 Proof. split. apply _. by intros []. Qed.
 
-(** Internalized properties *)
-Lemma excl_equivI {M} x y :
-  x ≡ y ⊣⊢@{uPredI M} match x, y with
-                      | Excl a, Excl b => a ≡ b
-                      | ExclBot, ExclBot => True
-                      | _, _ => False
-                      end.
-Proof.
-  uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
-Qed.
-Lemma excl_validI {M} x :
-  ✓ x ⊣⊢@{uPredI M} if x is ExclBot then False else True.
-Proof. uPred.unseal. by destruct x. Qed.
-
 (** Exclusive *)
 Global Instance excl_exclusive x : Exclusive x.
 Proof. by destruct x; intros n []. Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index b24b615059434fed786e3dd1db20d53d73a3f1ae..37b8f8b61ebaf1f686639939d3984f03fcfb7007 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -1,10 +1,9 @@
 From stdpp Require Export list gmap.
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import updates local_updates proofmode_classes.
-From iris.base_logic Require Import base_logic.
+From iris.algebra Require Import updates local_updates proofmode_classes big_op.
 From iris Require Import options.
 
-Section cofe.
+Section ofe.
 Context `{Countable K} {A : ofeT}.
 Implicit Types m : gmap K A.
 Implicit Types i : K.
@@ -96,9 +95,7 @@ Lemma insert_idN n m i x :
 Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
 
 (** Internalized properties *)
-Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢@{uPredI M} ∀ i, m1 !! i ≡ m2 !! i.
-Proof. by uPred.unseal. Qed.
-End cofe.
+End ofe.
 
 Arguments gmapO _ {_ _} _.
 
@@ -139,26 +136,6 @@ Proof.
   destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
 Qed.
 
-Lemma big_sepM2_ne_2 {PROP : bi} `{Countable K} (A B : ofeT)
-    (Φ Ψ : K → A → B → PROP) m1 m2 m1' m2' n :
-  m1 ≡{n}≡ m1' → m2 ≡{n}≡ m2' →
-  (∀ k y1 y1' y2 y2',
-    m1 !! k = Some y1 → m1' !! k = Some y1' → y1 ≡{n}≡ y1' →
-    m2 !! k = Some y2 → m2' !! k = Some y2' → y2 ≡{n}≡ y2' →
-    Φ k y1 y2 ≡{n}≡ Ψ k y1' y2') →
-  ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2)%I ≡{n}≡ ([∗ map] k ↦ y1;y2 ∈ m1';m2', Ψ k y1 y2)%I.
-Proof.
-  intros Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
-  { f_equiv; split; intros Hm k.
-    - trans (is_Some (m1 !! k)); [symmetry; apply: is_Some_ne; by f_equiv|].
-      rewrite Hm. apply: is_Some_ne; by f_equiv.
-    - trans (is_Some (m1' !! k)); [apply: is_Some_ne; by f_equiv|].
-      rewrite Hm. symmetry. apply: is_Some_ne; by f_equiv. }
-  apply big_opM_ne_2; [by f_equiv|].
-  intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
-    (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
-Qed.
-
 (* CMRA *)
 Section cmra.
 Context `{Countable K} {A : cmraT}.
@@ -253,18 +230,6 @@ Proof.
 Qed.
 Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin.
 
-(** Internalized properties *)
-Lemma gmap_validI {M} m : ✓ m ⊣⊢@{uPredI M} ∀ i, ✓ (m !! i).
-Proof. by uPred.unseal. Qed.
-Lemma singleton_validI {M} i x : ✓ {[ i := x ]} ⊣⊢@{uPredI M} ✓ x.
-Proof.
-  rewrite gmap_validI. apply: anti_symm.
-  - rewrite (bi.forall_elim i) lookup_singleton uPred.option_validI. done.
-  - apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
-    + rewrite lookup_singleton uPred.option_validI. done.
-    + rewrite lookup_singleton_ne // uPred.option_validI.
-      apply bi.True_intro.
-Qed.
 End cmra.
 
 Arguments gmapR _ {_ _} _.
diff --git a/theories/algebra/lib/excl_auth.v b/theories/algebra/lib/excl_auth.v
index 040eded52a8c288636e46c8fbe5600cf2dc1d2a2..307a841cc723daecc9f615611ffa9d504e752562 100644
--- a/theories/algebra/lib/excl_auth.v
+++ b/theories/algebra/lib/excl_auth.v
@@ -1,6 +1,5 @@
 From iris.algebra Require Export auth excl updates.
 From iris.algebra Require Import local_updates.
-From iris.base_logic Require Import base_logic.
 From iris Require Import options.
 
 (** Authoritative CMRA where the fragment is exclusively owned.
@@ -60,13 +59,6 @@ Section excl_auth.
   Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
   Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
 
-  Lemma excl_auth_agreeI {M} a b : ✓ (●E a ⋅ ◯E b) ⊢@{uPredI M} (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.
-
   Lemma excl_auth_frag_validN_op_1_l n a b : ✓{n} (◯E a ⋅ ◯E b) → False.
   Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
   Lemma excl_auth_frag_valid_op_1_l a b : ✓ (◯E a ⋅ ◯E b) → False.
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 36a6ea4ede9a145071d75904f9f99e14a4a4f2bc..f9e9ebe010aba57cb8fd23699ad2a05c3a3f0146 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -1,9 +1,7 @@
 From Coq.QArith Require Import Qcanon.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import view updates dfrac.
 From iris.algebra Require Export gmap dfrac.
 From iris.algebra Require Import local_updates proofmode_classes.
-From iris.base_logic Require Import base_logic.
 From iris Require Import options.
 
 (** * CMRA for a "view of a gmap".
@@ -317,25 +315,6 @@ Section lemmas.
     IsOp' (gmap_view_frag k dq v) (gmap_view_frag k dq1 v) (gmap_view_frag k dq2 v).
   Proof. rewrite /IsOp' /IsOp => ->. apply gmap_view_frag_op. Qed.
 
-  (** Internalized properties *)
-  Lemma gmap_view_both_validI M m k dq v :
-    ✓ (gmap_view_auth m ⋅ gmap_view_frag k dq v) ⊢@{uPredI M}
-    ✓ dq ∧ m !! k ≡ Some v.
-  Proof.
-    rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
-    intros n a. uPred.unseal. apply gmap_view_rel_lookup.
-  Qed.
-
-  Lemma gmap_view_frag_op_validI M k dq1 dq2 v1 v2 :
-    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊢@{uPredI M}
-      ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
-  Proof.
-    rewrite /gmap_view_frag -view_frag_op view_frag_validI.
-    rewrite singleton_op singleton_validI -pair_op uPred.prod_validI /=.
-    apply bi.and_mono; first done.
-    rewrite agree_validI agree_equivI. done.
-  Qed.
-
 End lemmas.
 
 (** Functor *)
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index d4a6f9067070b3db4151aa4f2a9c5b03fb714555..798a80daa4a3b7c97f6b6208a2ec00c357498616 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -1,10 +1,9 @@
 From stdpp Require Export list.
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import updates local_updates.
-From iris.base_logic Require Import base_logic.
+From iris.algebra Require Import updates local_updates big_op.
 From iris Require Import options.
 
-Section cofe.
+Section ofe.
 Context {A : ofeT}.
 Implicit Types l : list A.
 
@@ -94,10 +93,7 @@ Proof. inversion_clear 1; constructor. Qed.
 Global Instance cons_discrete x l : Discrete x → Discrete l → Discrete (x :: l).
 Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.
 
-(** Internalized properties *)
-Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢@{uPredI M} ∀ i, l1 !! i ≡ l2 !! i.
-Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
-End cofe.
+End ofe.
 
 Arguments listO : clear implicits.
 
@@ -139,22 +135,6 @@ Proof.
   destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
 Qed.
 
-Lemma big_sepL2_ne_2 {PROP : bi} {A B : ofeT}
-    (Φ Ψ : nat → A → B → PROP) l1 l2 l1' l2' n :
-  l1 ≡{n}≡ l1' → l2 ≡{n}≡ l2' →
-  (∀ k y1 y1' y2 y2',
-    l1 !! k = Some y1 → l1' !! k = Some y1' → y1 ≡{n}≡ y1' →
-    l2 !! k = Some y2 → l2' !! k = Some y2' → y2 ≡{n}≡ y2' →
-    Φ k y1 y2 ≡{n}≡ Ψ k y1' y2') →
-  ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)%I ≡{n}≡ ([∗ list] k ↦ y1;y2 ∈ l1';l2', Ψ k y1 y2)%I.
-Proof.
-  intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
-  { do 2 f_equiv; by apply: length_ne. }
-  apply big_opL_ne_2; [by f_equiv|].
-  intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
-    (?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
-Qed.
-
 (** Functor *)
 Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A → B) (l : list A) n :
   (∀ x, f x ≡{n}≡ g x) → f <$> l ≡{n}≡ g <$> l.
@@ -314,9 +294,6 @@ Section cmra.
   Global Instance list_core_id l : (∀ x : A, CoreId x) → CoreId l.
   Proof. intros Hyp; by apply list_core_id'. Qed.
 
-  (** Internalized properties *)
-  Lemma list_validI {M} l : ✓ l ⊣⊢@{uPredI M} ∀ i, ✓ (l !! i).
-  Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
 End cmra.
 
 Arguments listR : clear implicits.
diff --git a/theories/algebra/proofmode_classes.v b/theories/algebra/proofmode_classes.v
index 608b329e4e8bec79c5652dbe30ef26d821c70ec9..7cfbdc09bc8d6b993733ff324d5aa0914810b26d 100644
--- a/theories/algebra/proofmode_classes.v
+++ b/theories/algebra/proofmode_classes.v
@@ -1,5 +1,4 @@
 From iris.algebra Require Export cmra.
-From iris.proofmode Require Export classes.
 From iris Require Import options.
 
 (* There are various versions of [IsOp] with different modes:
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index 21541b73b361d30fe53b19a067a6ea8ed59f2585..a60cf84644febc67f527bc12cb889c0e679e5a4f 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -1,7 +1,5 @@
-From iris.proofmode Require Import tactics.
-From iris.algebra Require Export frac agree local_updates.
-From iris.algebra Require Import proofmode_classes.
-From iris.base_logic Require Import base_logic.
+From iris.algebra Require Export updates local_updates frac agree.
+From iris.algebra Require Import proofmode_classes big_op.
 From iris Require Import options.
 
 (** The view camera with fractional authoritative elements *)
@@ -428,62 +426,6 @@ Section cmra.
     ●V a1 ⋅ ◯V b1 ≼ ●V a2 ⋅ ◯V b2 ↔ a1 ≡ a2 ∧ b1 ≼ b2.
   Proof. rewrite view_both_frac_included. naive_solver. Qed.
 
-  (** Internalized properties *)
-  Lemma view_both_frac_validI_1 {M} (relI : uPred M) q a b :
-    (∀ n (x : M), rel n a b → relI n x) →
-    ✓ (●V{q} a ⋅ ◯V b) ⊢ ✓ q ∧ relI.
-  Proof.
-    intros Hrel. uPred.unseal. split=> n x _ /=.
-    rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
-  Qed.
-  Lemma view_both_frac_validI_2 {M} (relI : uPred M) q a b :
-    (∀ n (x : M), relI n x → rel n a b) →
-    ✓ q ∧ relI ⊢ ✓ (●V{q} a ⋅ ◯V b).
-  Proof.
-    intros Hrel. uPred.unseal. split=> n x _ /=.
-    rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
-  Qed.
-  Lemma view_both_frac_validI {M} (relI : uPred M) q a b :
-    (∀ n (x : M), rel n a b ↔ relI n x) →
-    ✓ (●V{q} a ⋅ ◯V b) ⊣⊢ ✓ q ∧ relI.
-  Proof.
-    intros. apply (anti_symm _);
-      [apply view_both_frac_validI_1|apply view_both_frac_validI_2]; naive_solver.
-  Qed.
-
-  Lemma view_both_validI_1 {M} (relI : uPred M) a b :
-    (∀ n (x : M), rel n a b → relI n x) →
-    ✓ (●V a ⋅ ◯V b) ⊢ relI.
-  Proof. intros. by rewrite view_both_frac_validI_1 // bi.and_elim_r. Qed.
-  Lemma view_both_validI_2 {M} (relI : uPred M) a b :
-    (∀ n (x : M), relI n x → rel n a b) →
-    relI ⊢ ✓ (●V a ⋅ ◯V b).
-  Proof.
-    intros. rewrite -view_both_frac_validI_2 // uPred.discrete_valid.
-    apply bi.and_intro; [|done]. by apply bi.pure_intro.
-  Qed.
-  Lemma view_both_validI {M} (relI : uPred M) a b :
-    (∀ n (x : M), rel n a b ↔ relI n x) →
-    ✓ (●V a ⋅ ◯V b) ⊣⊢ relI.
-  Proof.
-    intros. apply (anti_symm _);
-      [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
-  Qed.
-
-  Lemma view_auth_frac_validI {M} (relI : uPred M) q a :
-    (∀ n (x : M), relI n x ↔ rel n a ε) →
-    ✓ (●V{q} a) ⊣⊢ ✓ q ∧ relI.
-  Proof.
-    intros. rewrite -(right_id ε op (●V{q} a)). by apply view_both_frac_validI.
-  Qed.
-  Lemma view_auth_validI {M} (relI : uPred M) a :
-    (∀ n (x : M), relI n x ↔ rel n a ε) →
-    ✓ (●V a) ⊣⊢ relI.
-  Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.
-
-  Lemma view_frag_validI {M} b : ✓ (◯V b) ⊣⊢@{uPredI M} ✓ b.
-  Proof. by uPred.unseal. Qed.
-
   (** Updates *)
   Lemma view_update a b a' b' :
     (∀ n bf, rel n a (b ⋅ bf) → rel n a' (b' ⋅ bf)) →
diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
new file mode 100644
index 0000000000000000000000000000000000000000..9e2758efd58b32cf71f3322ba19c13f1d2f91c7c
--- /dev/null
+++ b/theories/base_logic/algebra.v
@@ -0,0 +1,250 @@
+From iris.algebra Require Import cmra view auth agree csum list excl gmap lib.excl_auth lib.gmap_view.
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import bi derived.
+From iris Require Import options.
+
+(** Internalized properties of our CMRA constructions. *)
+
+Section upred.
+Context {M : ucmraT}.
+
+Section gmap_ofe.
+  Context `{Countable K} {A : ofeT}.
+  Implicit Types m : gmap K A.
+  Implicit Types i : K.
+
+  Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢@{uPredI M} ∀ i, m1 !! i ≡ m2 !! i.
+  Proof. by uPred.unseal. Qed.
+End gmap_ofe.
+
+Section gmap_cmra.
+  Context `{Countable K} {A : cmraT}.
+  Implicit Types m : gmap K A.
+
+  Lemma gmap_validI m : ✓ m ⊣⊢@{uPredI M} ∀ i, ✓ (m !! i).
+  Proof. by uPred.unseal. Qed.
+  Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢@{uPredI M} ✓ x.
+  Proof.
+    rewrite gmap_validI. apply: anti_symm.
+    - rewrite (bi.forall_elim i) lookup_singleton uPred.option_validI. done.
+    - apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
+      + rewrite lookup_singleton uPred.option_validI. done.
+      + rewrite lookup_singleton_ne // uPred.option_validI.
+        apply bi.True_intro.
+  Qed.
+End gmap_cmra.
+
+Section list_ofe.
+  Context {A : ofeT}.
+  Implicit Types l : list A.
+
+  Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢@{uPredI M} ∀ i, l1 !! i ≡ l2 !! i.
+  Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
+End list_ofe.
+
+Section list_cmra.
+  Context {A : ucmraT}.
+  Implicit Types l : list A.
+
+  Lemma list_validI l : ✓ l ⊣⊢@{uPredI M} ∀ i, ✓ (l !! i).
+  Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
+End list_cmra.
+
+Section excl.
+  Context {A : ofeT}.
+  Implicit Types a b : A.
+  Implicit Types x y : excl A.
+
+  Lemma excl_equivI x y :
+    x ≡ y ⊣⊢@{uPredI M} match x, y with
+                        | Excl a, Excl b => a ≡ b
+                        | ExclBot, ExclBot => True
+                        | _, _ => False
+                        end.
+  Proof.
+    uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
+  Qed.
+  Lemma excl_validI x :
+    ✓ x ⊣⊢@{uPredI M} if x is ExclBot then False else True.
+  Proof. uPred.unseal. by destruct x. Qed.
+End excl.
+
+Section agree.
+  Context {A : ofeT}.
+  Implicit Types a b : A.
+  Implicit Types x y : agree A.
+
+  Lemma agree_equivI a b : to_agree a ≡ to_agree b ⊣⊢@{uPredI M} (a ≡ b).
+  Proof.
+    uPred.unseal. do 2 split.
+    - intros Hx. exact: (inj to_agree).
+    - intros Hx. exact: to_agree_ne.
+  Qed.
+  Lemma agree_validI x y : ✓ (x ⋅ y) ⊢@{uPredI M} x ≡ y.
+  Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
+
+  Lemma to_agree_uninjI x : ✓ x ⊢@{uPredI M} ∃ a, to_agree a ≡ x.
+  Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
+End agree.
+
+Section csum_ofe.
+  Context {A B : ofeT}.
+  Implicit Types a : A.
+  Implicit Types b : B.
+
+  Lemma csum_equivI (x y : csum A B) :
+    x ≡ y ⊣⊢@{uPredI M} match x, y with
+                        | Cinl a, Cinl a' => a ≡ a'
+                        | Cinr b, Cinr b' => b ≡ b'
+                        | CsumBot, CsumBot => True
+                        | _, _ => False
+                        end.
+  Proof.
+    uPred.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 : cmraT}.
+  Implicit Types a : A.
+  Implicit Types b : B.
+
+  Lemma csum_validI (x : csum A B) :
+    ✓ x ⊣⊢@{uPredI M} match x with
+                      | Cinl a => ✓ a
+                      | Cinr b => ✓ b
+                      | CsumBot => False
+                      end.
+  Proof. uPred.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.
+
+  Lemma view_both_frac_validI_1 (relI : uPred M) q a b :
+    (∀ n (x : M), rel n a b → relI n x) →
+    ✓ (●V{q} a ⋅ ◯V b : view rel) ⊢ ✓ q ∧ relI.
+  Proof.
+    intros Hrel. uPred.unseal. split=> n x _ /=.
+    rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
+  Qed.
+  Lemma view_both_frac_validI_2 (relI : uPred M) q a b :
+    (∀ n (x : M), relI n x → rel n a b) →
+    ✓ q ∧ relI ⊢ ✓ (●V{q} a ⋅ ◯V b : view rel).
+  Proof.
+    intros Hrel. uPred.unseal. split=> n x _ /=.
+    rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
+  Qed.
+  Lemma view_both_frac_validI (relI : uPred M) q a b :
+    (∀ n (x : M), rel n a b ↔ relI n x) →
+    ✓ (●V{q} a ⋅ ◯V b : view rel) ⊣⊢ ✓ q ∧ relI.
+  Proof.
+    intros. apply (anti_symm _);
+      [apply view_both_frac_validI_1|apply view_both_frac_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_frac_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_frac_validI_2 // uPred.discrete_valid.
+    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_frac_validI (relI : uPred M) q a :
+    (∀ n (x : M), relI n x ↔ rel n a ε) →
+    ✓ (●V{q} a : view rel) ⊣⊢ ✓ q ∧ relI.
+  Proof.
+    intros. rewrite -(right_id ε op (●V{q} a)). by apply view_both_frac_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 b : ✓ (◯V b : view rel) ⊣⊢@{uPredI M} ✓ b.
+  Proof. by uPred.unseal. Qed.
+End view.
+
+Section auth.
+  Context {A : ucmraT}.
+  Implicit Types a b : A.
+  Implicit Types x y : auth A.
+
+  (** Internalized properties *)
+  Lemma auth_auth_frac_validI q a : ✓ (●{q} a) ⊣⊢@{uPredI M} ✓ q ∧ ✓ a.
+  Proof.
+    apply view_auth_frac_validI=> n. uPred.unseal; split; [|by intros [??]].
+    split; [|done]. apply ucmra_unit_leastN.
+  Qed.
+  Lemma auth_auth_validI a : ✓ (● a) ⊣⊢@{uPredI M} ✓ a.
+  Proof.
+    by rewrite auth_auth_frac_validI uPred.discrete_valid bi.pure_True // left_id.
+  Qed.
+
+  Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢@{uPredI M} ✓ a.
+  Proof. apply view_frag_validI. Qed.
+
+  Lemma auth_both_frac_validI q a b :
+    ✓ (●{q} a ⋅ ◯ b) ⊣⊢@{uPredI M} ✓ q ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+  Proof. apply view_both_frac_validI=> n. by uPred.unseal. Qed.
+  Lemma auth_both_validI a b :
+    ✓ (● a ⋅ ◯ b) ⊣⊢@{uPredI M} (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+  Proof.
+    by rewrite auth_both_frac_validI uPred.discrete_valid bi.pure_True // left_id.
+  Qed.
+
+End auth.
+
+Section excl_auth.
+  Context {A : ofeT}.
+  Implicit Types a b : A.
+
+  Lemma excl_auth_agreeI a b : ✓ (●E a ⋅ ◯E b) ⊢@{uPredI M} (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 : ofeT}.
+  Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
+
+  Lemma gmap_view_both_validI m k dq v :
+    ✓ (gmap_view_auth m ⋅ gmap_view_frag k dq v) ⊢@{uPredI M}
+    ✓ dq ∧ m !! k ≡ Some v.
+  Proof.
+    rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
+    intros n a. uPred.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) ⊢@{uPredI M}
+      ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
+  Proof.
+    rewrite /gmap_view_frag -view_frag_op view_frag_validI.
+    rewrite singleton_op singleton_validI -pair_op uPred.prod_validI /=.
+    apply bi.and_mono; first done.
+    rewrite agree_validI agree_equivI. done.
+  Qed.
+End gmap_view.
+
+End upred.
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index d6fea5a090b9708672ca42148eaa11c0a2581e8d..2c44469532d4eb17118502053e27b2b492d15131 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,5 +1,5 @@
 From iris.bi Require Export bi.
-From iris.base_logic Require Export derived proofmode.
+From iris.base_logic Require Export derived proofmode algebra.
 From iris Require Import options.
 
 (* The trick of having multiple [uPred] modules, which are all exported in
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index e600610dee00db9f1b2b7ef343c5238bd9ca5331..66684fb4d093b24c50a4faebf70fe4b73ce11001 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Import functions gmap proofmode_classes.
+From iris.proofmode Require Import classes.
 From iris.base_logic.lib Require Export iprop.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index d9f3a0e981aa046d1a129e8aa7bbfe5b3ba1713a..04d05d104117f3e38cc3341aa986e6c4fbeb5de6 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Import proofmode_classes.
+From iris.proofmode Require Import classes.
 From iris.base_logic Require Export derived.
 From iris Require Import options.
 
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 60a10ee1ba47eab16fc0274a7db3de2c947f1a90..5f2bc2e77d3ddd1171110558857583e9731a2f10 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1,6 +1,7 @@
 From stdpp Require Import countable fin_sets functions.
-From iris.bi Require Import derived_laws_later.
 From iris.algebra Require Export big_op.
+From iris.algebra Require Import list gmap.
+From iris.bi Require Import derived_laws_later.
 From iris Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
@@ -618,6 +619,22 @@ Section sep_list2.
   Proof. rewrite big_sepL2_alt. apply _. Qed.
 End sep_list2.
 
+Lemma big_sepL2_ne_2 {A B : ofeT}
+    (Φ Ψ : nat → A → B → PROP) l1 l2 l1' l2' n :
+  l1 ≡{n}≡ l1' → l2 ≡{n}≡ l2' →
+  (∀ k y1 y1' y2 y2',
+    l1 !! k = Some y1 → l1' !! k = Some y1' → y1 ≡{n}≡ y1' →
+    l2 !! k = Some y2 → l2' !! k = Some y2' → y2 ≡{n}≡ y2' →
+    Φ k y1 y2 ≡{n}≡ Ψ k y1' y2') →
+  ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)%I ≡{n}≡ ([∗ list] k ↦ y1;y2 ∈ l1';l2', Ψ k y1 y2)%I.
+Proof.
+  intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
+  { do 2 f_equiv; by apply: length_ne. }
+  apply big_opL_ne_2; [by f_equiv|].
+  intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
+    (?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
+Qed.
+
 Section and_list.
   Context {A : Type}.
   Implicit Types l : list A.
@@ -1457,6 +1474,26 @@ Section map2.
   Proof. intros. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
 End map2.
 
+Lemma big_sepM2_ne_2 `{Countable K} (A B : ofeT)
+    (Φ Ψ : K → A → B → PROP) m1 m2 m1' m2' n :
+  m1 ≡{n}≡ m1' → m2 ≡{n}≡ m2' →
+  (∀ k y1 y1' y2 y2',
+    m1 !! k = Some y1 → m1' !! k = Some y1' → y1 ≡{n}≡ y1' →
+    m2 !! k = Some y2 → m2' !! k = Some y2' → y2 ≡{n}≡ y2' →
+    Φ k y1 y2 ≡{n}≡ Ψ k y1' y2') →
+  ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2)%I ≡{n}≡ ([∗ map] k ↦ y1;y2 ∈ m1';m2', Ψ k y1 y2)%I.
+Proof.
+  intros Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
+  { f_equiv; split; intros Hm k.
+    - trans (is_Some (m1 !! k)); [symmetry; apply: is_Some_ne; by f_equiv|].
+      rewrite Hm. apply: is_Some_ne; by f_equiv.
+    - trans (is_Some (m1' !! k)); [apply: is_Some_ne; by f_equiv|].
+      rewrite Hm. symmetry. apply: is_Some_ne; by f_equiv. }
+  apply big_opM_ne_2; [by f_equiv|].
+  intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
+    (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
+Qed.
+
 (** ** Big ops over finite sets *)
 Section gset.
   Context `{Countable A}.