diff --git a/opam b/opam
index 46637bafbf47a6922f38b71ed1c90230419898cd..098d46ae23cea90933ae57bb073cfea2b202e6c5 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2020-10-15.2.f4060bb5") | (= "dev") }
+  "coq-iris" { (= "dev.2020-10-20.2.c65b38ea") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 83aa92cb37df25a37eae8e9cb2acb70931b53336..dc46d11a971370e675484a215bfe587367962f0c 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -46,8 +46,8 @@ Section refinement.
 
   Lemma ticket_nondup γ n : ticket γ n -∗ ticket γ n -∗ False.
   Proof.
-    iIntros "Ht1 Ht2".
-    iDestruct (own_valid_2 with "Ht1 Ht2") as %?%gset_disj_valid_op.
+    iIntros "Ht1 Ht2". iDestruct (own_valid_2 with "Ht1 Ht2")
+      as %?%auth_frag_op_valid_1%gset_disj_valid_op.
     set_solver.
   Qed.
 
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 5e76800d9dec7cb3c723b617e1383fce33936e5c..54c7ace7273e9714fc353693d19c93185bd780d1 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -165,12 +165,10 @@ Section mapsto.
   Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
     apply bi.wand_intro_r.
-    rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
-    f_equiv=> /=.
-    rewrite -pair_op singleton_op right_id -pair_op.
-    move=> [_ Hv]. move:Hv => /=.
-    rewrite singleton_valid.
-    by move=> [_] /to_agree_op_inv_L [->].
+    rewrite heapS_mapsto_eq -own_op own_valid uPred.discrete_valid. f_equiv.
+    rewrite auth_frag_op_valid -pair_op singleton_op -pair_op.
+    rewrite pair_valid singleton_valid pair_valid to_agree_op_valid_L.
+    by intros [_ [_ [=]]].
   Qed.
 
   Lemma mapstoS_valid l q v : l ↦ₛ{q} v -∗ ✓ q.