diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 8556ed2d8aff1fbedb4e848e53d5c0d1520cc48d..bc52dd8e60fbbe57cda7e6b76b1ba056b18af4cb 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export view.
+From iris.algebra Require Export view frac.
 From iris.algebra Require Import proofmode_classes big_op.
 From iris.prelude Require Import options.
 
@@ -86,6 +86,8 @@ Section auth.
   Context {A : ucmra}.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
+  Implicit Types q : frac.
+  Implicit Types dq : dfrac.
 
   Global Instance auth_auth_ne dq : NonExpansive (@auth_auth A dq).
   Proof. rewrite /auth_auth. apply _. Qed.
diff --git a/iris/algebra/lib/gset_bij.v b/iris/algebra/lib/gset_bij.v
index a692969163f3756811452b64e5e261ee2c87e6a7..c6d29f62f8f5fdb09b785e046aec0c609196e685 100644
--- a/iris/algebra/lib/gset_bij.v
+++ b/iris/algebra/lib/gset_bij.v
@@ -114,6 +114,7 @@ Section gset_bij.
   Context `{Countable A, Countable B}.
   Implicit Types (a:A) (b:B).
   Implicit Types (L : gset (A*B)).
+  Implicit Types dq : dfrac.
 
   Global Instance gset_bij_elem_core_id a b : CoreId (gset_bij_elem a b).
   Proof. apply _. Qed.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 6e857ab4fc45337fbea8b770224df0575fc1b671..77c636d2a8eac8a8223f1b49c0a729388e240acb 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export updates local_updates dfrac agree.
+From iris.algebra Require Export updates local_updates frac dfrac agree.
 From iris.algebra Require Import proofmode_classes big_op.
 From iris.prelude Require Import options.
 
@@ -151,6 +151,8 @@ Section cmra.
   Implicit Types ag : option (dfrac * agree A).
   Implicit Types b : B.
   Implicit Types x y : view rel.
+  Implicit Types q : frac.
+  Implicit Types dq : dfrac.
 
   Global Instance view_auth_ne dq : NonExpansive (@view_auth A B rel dq).
   Proof. solve_proper. Qed.
@@ -390,9 +392,9 @@ Section cmra.
     ●V{dq1} a1 ≼{n} ●V{dq2} a2 ⋅ ◯V b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2.
   Proof.
     split.
-    - intros [[[[qf agf]|] bf]
+    - intros [[[[dqf agf]|] bf]
         [[?%(discrete_iff _ _) ?]%(inj Some) _]]; simplify_eq/=.
-      + split; [left; apply cmra_included_l|]. apply to_agree_includedN. by exists agf.
+      + split; [left; apply (cmra_included_l dq1)|]. apply to_agree_includedN. by exists agf.
       + split; [right; done|]. by apply (inj to_agree).
     - intros [[[? ->]| ->] ->].
       + rewrite view_auth_dfrac_op -assoc. apply cmra_includedN_l.