diff --git a/atomic.v b/atomic.v
index ee42b9071f07ef2716d3a5ff4e9c3ec4bdaea5af..be3168a8b4d0952d4d4b3a0c369fc4dfe912bb99 100644
--- a/atomic.v
+++ b/atomic.v
@@ -18,6 +18,6 @@ Section atomic.
     (∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
                        α x ★
                        ((α x ={Ei, Eo}=★ P) ∧
-                        (∀ v, β x v ={Ei, Eo}=★ Q x v))
-     ) -★ {{ P }} e @ ⊤ {{ v, (∃ x: A, Q x v) }})%I.
+                        (∀ v, β x v ={Ei, Eo}=★ Q v))
+     ) -★ {{ P }} e @ ⊤ {{ Q }})%I.
 End atomic.
diff --git a/atomic_incr.v b/atomic_incr.v
index 9b17c020c159c0cf366e2f03f04b80dcf186b847..6e5dbba04034890dba2a460344dc34dc0f27f4e4 100644
--- a/atomic_incr.v
+++ b/atomic_incr.v
@@ -46,7 +46,7 @@ Section incr.
       iSpecialize ("Hvs'" $! #x').
       wp_cas_suc.
       iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
-      iModIntro. wp_if. by iExists x'.
+      iModIntro. wp_if. done.
     - iDestruct "Hvs'" as "[Hvs' _]".
       wp_cas_fail.
       iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
@@ -80,7 +80,7 @@ Section user.
     (* prove worker triple *)
     iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//.
     rewrite /incr_triple /atomic_triple.
-    iSpecialize ("Hincr"  $! True%I (fun _ _ => True%I) with "[]").
+    iSpecialize ("Hincr"  $! True%I (fun _ => True%I) with "[]").
     - iIntros "!# _".
       (* open the invariant *)
       iInv N as (x') ">Hl'" "Hclose".
diff --git a/atomic_sync.v b/atomic_sync.v
index 0466de9b523725a5cf9e017e2e0211c0556d4d90..02c6b22b0b35f9495b205cd6e6d8079ca36604ff 100644
--- a/atomic_sync.v
+++ b/atomic_sync.v
@@ -57,9 +57,9 @@ Section atomic_sync.
     iIntros (f). iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
     iIntros (f') "#Hsynced {Hsyncer}".
     iAlways. iIntros (α β x) "#Hseq".
-    iIntros (P Q) "#Hvss !# HP". 
+    iIntros (P Q) "#Hvss !# HP".
     (* TODO: Why can't I iApply "Hsynced"? *)
-    iSpecialize ("Hsynced" $! P (fun v => ∃ x, Q x v)%I x).
+    iSpecialize ("Hsynced" $! P Q x).
     iApply wp_wand_r. iSplitL "HP".
     - iApply ("Hsynced" with "[]")=>//.
       iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[HÏ• Hg1]".
@@ -81,7 +81,7 @@ Section atomic_sync.
         apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. }
       iMod ("Hvs2" with "[Hg1 Hβ]").
       { iExists g'. iFrame. }
-      iModIntro. iSplitL "Hg2 HÏ•'"; last by iExists g''.
+      iModIntro. iSplitL "Hg2 HÏ•'"; last done.
       iExists g'. by iFrame.
     - iIntros (?) "?". done.
   Qed.
diff --git a/peritem.v b/peritem.v
index f58658ede893a5f098f2c1f52f3bc836efa1611f..ce12b4741d39325b14b116e7a21cf689b32bbf3a 100644
--- a/peritem.v
+++ b/peritem.v
@@ -133,7 +133,7 @@ Lemma new_stack_spec' Φ RI:
   Proof.
     iIntros (HN) "(#Hh & HRx & #? & HΦ)".
     iDestruct (push_atomic_spec N s x with "Hh") as "Hpush"=>//.
-    iSpecialize ("Hpush" $! (R x) (fun _ ret => (∃ hd, evs γ hd x) ★ ret = #())%I with "[]").
+    iSpecialize ("Hpush" $! (R x) (fun ret => (∃ hd, evs γ hd x) ★ ret = #())%I with "[]").
     - iIntros "!# Rx".
       (* open the invariant *)
       iInv N as "[IH1 ?]" "Hclose".
@@ -180,7 +180,7 @@ Lemma new_stack_spec' Φ RI:
         iModIntro. iSplitL; last auto. by iExists hd'.
     - iApply wp_wand_r. iSplitL "HRx Hpush".
       + by iApply "Hpush".
-      + iIntros (?) "H". iDestruct "H" as (_) "[? %]". subst.
+      + iIntros (?) "[? %]". subst.
         by iApply "HΦ".
   Qed.