diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index b76c2e6b56a9dcb0e8e9e30f0ba465bf953a3e86..ea3f9e371c7beee72605ac71141c793d4a99d1fd 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -130,6 +130,13 @@ Section auth.
   Proof. apply view_frag_mono. Qed.
   Lemma auth_frag_core a : core (â—¯ a) = â—¯ (core a).
   Proof. apply view_frag_core. Qed.
+  Lemma auth_both_core_discarded a b :
+    core (●□ a ⋅ ◯ b) ≡ ●□ a ⋅ ◯ (core b).
+  Proof. apply view_both_core_discarded. Qed.
+  Lemma auth_both_core_frac q a b :
+    core (●{#q} a ⋅ ◯ b) ≡ ◯ (core b).
+  Proof. apply view_both_core_frac. Qed.
+
   Global Instance auth_auth_core_id a : CoreId (●□ a).
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 44b97fb7fa382abc919f0d161c51bd976c59d783..c260a1b21c16ad7e56478ea94f2812a3eb3ac2a9 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -209,6 +209,16 @@ Section cmra.
       | Some (dq, ag) => ✓{n} dq ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
       | None => ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
+  Local Definition view_pcore_eq :
+      pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x)))
+    := eq_refl _.
+  Local Definition view_core_eq :
+      core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x))
+    := eq_refl _.
+  Local Definition view_op_eq :
+      op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y)
+                       (view_frag_proj x â‹… view_frag_proj y)
+    := eq_refl _.
 
   Lemma view_cmra_mixin : CmraMixin (view rel).
   Proof.
@@ -285,6 +295,13 @@ Section cmra.
   Proof. intros [c ->]. rewrite view_frag_op. apply cmra_included_l. Qed.
   Lemma view_frag_core b : core (â—¯V b) = â—¯V (core b).
   Proof. done. Qed.
+  Lemma view_both_core_discarded a b :
+    core (●V□ a ⋅ ◯V b) ≡ ●V□ a ⋅ ◯V (core b).
+  Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
+  Lemma view_both_core_frac q a b :
+    core (●V{#q} a ⋅ ◯V b) ≡ ◯V (core b).
+  Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
+
   Global Instance view_auth_core_id a : CoreId (●V□ a).
   Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
   Global Instance view_frag_core_id b : CoreId b → CoreId (◯V b).