diff --git a/algebra/auth.v b/algebra/auth.v
index 29760ee65f234ebf447e5c1d6c1e1fc8025ce2d6..0397b82dcf61a518fe51abcc1e753ac8283f7683 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -148,11 +148,11 @@ Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
 
 Lemma auth_update a a' b b' :
-  (∀ n af, ✓{n} a → a ={n}= a' ⋅ af → b ={n}= b' ⋅ af ∧ ✓{n} b) →
+  (∀ n af, ✓{S n} a → a ={S n}= a' ⋅ af → b ={S n}= b' ⋅ af ∧ ✓{S n} b) →
   ● a ⋅ ◯ a' ~~> ● b ⋅ ◯ b'.
 Proof.
-  move=> Hab [[] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
-  destruct (Hab (S n) (bf1 â‹… bf2)) as [Ha' ?]; auto.
+  move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
+  destruct (Hab n (bf1 â‹… bf2)) as [Ha' ?]; auto.
   { by rewrite Ha left_id associative. }
   split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
 Qed.