diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 3166745c3e13cdfeb1a351acbd0f6a049cf40a93..82b2cabc0f41575c1a5e46e330887c2dc50fdad5 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -131,7 +131,7 @@ Section auth.
   Lemma auth_frag_core a : core (â—¯ a) = â—¯ (core a).
   Proof. apply view_frag_core. Qed.
   Lemma auth_both_core_discarded a b :
-    core (●{DfracDiscarded} a ⋅ ◯ b) ≡ ●{DfracDiscarded} a ⋅ ◯ (core 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).
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index cca42710d54a736697a52000892c7434ef9d8608..0406fc976044a22d79e4e271fce54afe7337d668 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -296,7 +296,7 @@ Section cmra.
   Lemma view_frag_core b : core (â—¯V b) = â—¯V (core b).
   Proof. done. Qed.
   Lemma view_both_core_discarded a b :
-    core (●V{DfracDiscarded} a ⋅ ◯V b) ≡ ●V{DfracDiscarded} a ⋅ ◯V (core 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).