use notation

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).

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).