diff --git a/iris_core.v b/iris_core.v
index d2f8e2586ada901e3cdb191b7b7c8679d80aa81a..6d2a8e2d21dbf17f1f6fc2879b0e25a0285f98af 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -348,29 +348,32 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
     Definition state_sat (r: option res) σ: Prop := match r with
     | Some (ex_own s, _) => s = σ
     | _ => False
-    end.
+                                                    end.
+
+    Global Instance state_sat_dist : Proper (equiv ==> equiv ==> iff) state_sat.
+    Proof.
+      intros r1 r2 EQr σ1 σ2 EQσ; apply ores_equiv_eq in EQr. rewrite EQσ, EQr. tauto.
+    Qed.
 
     Global Instance preo_unit : preoType () := disc_preo ().
 
-    Program Definition wsat (σ : state) (m : mask) (r s : option res) (w : Wld) : UPred () :=
-      â–¹ (mkUPred (fun n _ =>
-                    state_sat (r · s) σ
-                    /\ exists rs : nat -f> res,
-                         comp_map rs == s /\
-                         forall i (Hm : m i),
+    Program Definition wsat (σ : state) (m : mask) (r : option res) (w : Wld) : UPred () :=
+      â–¹ (mkUPred (fun n _ => exists rs : nat -f> res,
+                    state_sat (r · (comp_map rs)) σ
+                      /\ forall i (Hm : m i),
                            (i ∈ dom rs <-> i ∈ dom w) /\
                            forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
                              ı π w n ri) _).
     Next Obligation.
-      intros n1 n2 _ _ HLe _ [HES HRS]; split; [assumption |].
+      intros n1 n2 _ _ HLe _ [rs [HLS HRS] ]. exists rs; split; [assumption|].
       setoid_rewrite HLe; eassumption.
     Qed.
 
-    Global Instance wsat_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv ==> equiv) (wsat σ).
+    Global Instance wsat_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv) (wsat σ).
     Proof.
-      intros m1 m2 EQm r r' EQr s s' EQs w1 w2 EQw [| n] []; [reflexivity |];
-      apply ores_equiv_eq in EQr; apply ores_equiv_eq in EQs; subst r' s'.
-      split; intros [HES [rs [HE HM] ] ]; (split; [tauto | clear HES; exists rs]).
+      intros m1 m2 EQm r r' EQr w1 w2 EQw [| n] []; [reflexivity |];
+      apply ores_equiv_eq in EQr; subst r'.
+      split; intros [rs [HE HM] ]; exists rs.
       - split; [assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
         destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
         rewrite fdLookup_in; setoid_rewrite EQw; rewrite <- fdLookup_in; reflexivity.
@@ -379,10 +382,10 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
         rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
     Qed.
 
-    Global Instance wsat_dist n σ m r s : Proper (dist n ==> dist n) (wsat σ m r s).
+    Global Instance wsat_dist n σ m r : Proper (dist n ==> dist n) (wsat σ m r).
     Proof.
       intros w1 w2 EQw [| n'] [] HLt; [reflexivity |]; destruct n as [| n]; [now inversion HLt |].
-      split; intros [HES [rs [HE HM] ] ]; (split; [tauto | clear HES; exists rs]).
+      split; intros [rs [HE HM] ]; exists rs.
       - split; [assumption | split; [rewrite <- (domeq _ _ _ EQw); apply HM, Hm |] ].
         intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
         assert (EQÏ€ := EQw i); rewrite HLw in EQÏ€; clear HLw.
@@ -399,10 +402,10 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
         apply HR; [reflexivity | assumption].
     Qed.
 
-    Lemma wsat_not_empty σ m r s w k (HN : r · s == 0) :
-      ~ wsat σ m r s w (S k) tt.
+    Lemma wsat_not_empty σ m (r: option res) w k (HN : r == 0) :
+      ~ wsat σ m r w (S k) tt.
     Proof.
-      intros [HD _]; apply ores_equiv_eq in HN; setoid_rewrite HN in HD.
+      intros [rs [HD _] ]; apply ores_equiv_eq in HN. setoid_rewrite HN in HD.
       exact HD.
     Qed.
 
diff --git a/iris_vs.v b/iris_vs.v
index 894da315b0486113885330760f83586c759b93b3..3958f855720b46ea37d966b9fd00b4dbbbe07d89 100644
--- a/iris_vs.v
+++ b/iris_vs.v
@@ -13,22 +13,22 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
     Local Obligation Tactic := intros.
 
     Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
-      mkUPred (fun n r => forall w1 rf s mf σ k (HSub : w ⊑ w1) (HLe : k < n)
+      mkUPred (fun n r => forall w1 rf mf σ k (HSub : w ⊑ w1) (HLe : k < n)
                                  (HD : mf # m1 ∪ m2)
-                                 (HE : wsat σ (m1 ∪ mf) (Some r · rf) s w1 @ S k),
-                          exists w2 r' s',
+                                 (HE : wsat σ (m1 ∪ mf) (Some r · rf) w1 @ S k),
+                          exists w2 r',
                             w1 ⊑ w2 /\ p w2 (S k) r'
-                            /\ wsat σ (m2 ∪ mf) (Some r' · rf) s' w2 @ S k) _.
+                            /\ wsat σ (m2 ∪ mf) (Some r' · rf) w2 @ S k) _.
     Next Obligation.
       intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
-      destruct (HP w1 (Some rd · rf) s mf σ k) as [w2 [r1' [s' [HW [HP' HE'] ] ] ] ];
+      destruct (HP w1 (Some rd · rf) mf σ k) as [w2 [r1' [HW [HP' HE'] ] ] ];
         try assumption; [now eauto with arith | |].
       - eapply wsat_equiv, HE; try reflexivity.
         rewrite assoc, (comm (Some r1)), HR; reflexivity.
       - rewrite assoc, (comm (Some r1')) in HE'.
         destruct (Some rd · Some r1') as [r2' |] eqn: HR';
           [| apply wsat_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
-        exists w2 r2' s'; split; [assumption | split; [| assumption] ].
+        exists w2 r2'; split; [assumption | split; [| assumption] ].
         eapply uni_pred, HP'; [| exists rd; rewrite HR']; reflexivity.
     Qed.
 
@@ -45,19 +45,19 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
       intros w1 w2 EQw n' r HLt; destruct n as [| n]; [now inversion HLt |]; split; intros HP w2'; intros.
       - symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
         assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
-        edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
+        edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
         + eapply wsat_dist, HE; [symmetry; eassumption | now eauto with arith].
         + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
           assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
-          exists (extend w1'' w2') r' s'; split; [assumption | split].
+          exists (extend w1'' w2') r'; split; [assumption | split].
           * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
           * eapply wsat_dist, HE'; [symmetry; eassumption | now eauto with arith].
       - assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
-        edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
+        edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
         + eapply wsat_dist, HE; [symmetry; eassumption | now eauto with arith].
         + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
           assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
-          exists (extend w1'' w2') r' s'; split; [assumption | split].
+          exists (extend w1'' w2') r'; split; [assumption | split].
           * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
           * eapply wsat_dist, HE'; [symmetry; eassumption | now eauto with arith].
     Qed.
@@ -72,10 +72,10 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
     Qed.
     Next Obligation.
       intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
-      - edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
+      - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
         clear HP; repeat (eexists; try eassumption); [].
         apply EQp; [now eauto with arith | assumption].
-      - edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
+      - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
         clear HP; repeat (eexists; try eassumption); [].
         apply EQp; [now eauto with arith | assumption].
     Qed.
@@ -99,7 +99,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
     Proof.
       intros w' n r1 HTL w HSub; rewrite HSub in HTL; clear w' HSub.
       intros np rp HLe HS Hp w1; intros.
-      exists w1 rp s; split; [reflexivity | split; [| assumption] ]; clear HE HD.
+      exists w1 rp; split; [reflexivity | split; [| assumption] ]; clear HE HD.
       destruct np as [| np]; [now inversion HLe0 |]; simpl in Hp.
       unfold lt in HLe0; rewrite HLe0.
       rewrite <- HSub; apply HTL, Hp; [reflexivity | assumption].
@@ -114,16 +114,14 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
       apply ı in HInv; rewrite (isoR p) in HInv.
       (* get rid of the invisible 1/2 *)
       do 8 red in HInv.
-      destruct HE as [HES [rs [HE HM] ] ].
+      destruct HE as [rs [HE HM] ].
       destruct (rs i) as [ri |] eqn: HLr.
       - rewrite comp_map_remove with (i := i) (r := ri) in HE by assumption.
-        assert (HR : Some r · rf · s == Some r · Some ri · rf · comp_map (fdRemove i rs))
-          by (rewrite <- HE, assoc, <- (assoc (Some r)), (comm rf), assoc; reflexivity).
-        apply ores_equiv_eq in HR; setoid_rewrite HR in HES; clear HR.
+        rewrite assoc, <- (assoc (Some r)), (comm rf), assoc in HE.
         destruct (Some r · Some ri) as [rri |] eqn: HR;
-          [| erewrite !pcm_op_zero in HES by apply _; now contradiction].
-        exists w' rri (comp_map (fdRemove i rs)); split; [reflexivity |].
-        split; [| split; [assumption |] ].
+          [| erewrite !pcm_op_zero in HE by apply _; now contradiction].
+        exists w' rri; split; [reflexivity |].
+        split.
         + simpl; eapply HInv; [now auto with arith |].
           eapply uni_pred, HM with i;
             [| exists r; rewrite <- HR | | | rewrite HLr]; try reflexivity; [|].
@@ -131,7 +129,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
             destruct (Peano_dec.eq_nat_dec i i); tauto.
           * specialize (HSub i); rewrite HLu in HSub.
             symmetry; destruct (w' i); [assumption | contradiction].
-        + exists (fdRemove i rs); split; [reflexivity | intros j Hm].
+        + exists (fdRemove i rs); split; [assumption | intros j Hm].
           destruct Hm as [| Hm]; [contradiction |]; specialize (HD j); simpl in HD.
           unfold mask_sing, mask_set in HD; destruct (Peano_dec.eq_nat_dec i j);
           [subst j; contradiction HD; tauto | clear HD].
@@ -152,19 +150,17 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
       apply ı in HInv; rewrite (isoR p) in HInv.
       (* get rid of the invisible 1/2 *)
       do 8 red in HInv.
-      destruct HE as [HES [rs [HE HM] ] ].
-      exists w' (pcm_unit _) (Some r · s); split; [reflexivity | split; [exact I |] ].
-      assert (HR' : Some r · rf · s = rf · (Some r · s))
-        by (eapply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
-      setoid_rewrite HR' in HES; erewrite pcm_op_unit by apply _.
-      split; [assumption |].
+      destruct HE as [rs [HE HM] ].
+      exists w' (pcm_unit _); split; [reflexivity | split; [exact I |] ].
+      rewrite (comm (Some r)), <-assoc in HE.
       remember (match rs i with Some ri => ri | None => pcm_unit _ end) as ri eqn: EQri.
       destruct (Some ri · Some r) as [rri |] eqn: EQR.
       - exists (fdUpdate i rri rs); split; [| intros j Hm].
-        + symmetry; rewrite <- HE; clear - EQR EQri; destruct (rs i) as [rsi |] eqn: EQrsi; subst;
-          [eapply comp_map_insert_old; [eassumption | rewrite <- EQR; reflexivity] |].
-          erewrite pcm_op_unit in EQR by apply _; rewrite EQR.
-          now apply comp_map_insert_new.
+        + erewrite pcm_op_unit by apply _.
+          clear - HE EQR EQri. destruct (rs i) as [rsi |] eqn: EQrsi; subst.
+          * erewrite <-comp_map_insert_old; try eassumption. rewrite<- EQR; reflexivity.
+          * erewrite <-comp_map_insert_new; try eassumption. rewrite <-EQR.
+            erewrite pcm_op_unit by apply _. assumption.
         + specialize (HD j); unfold mask_sing, mask_set in *; simpl in Hm, HD.
           destruct (Peano_dec.eq_nat_dec i j);
             [subst j; clear Hm |
@@ -184,9 +180,9 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
           exists rd; assumption.
       - destruct (rs i) as [rsi |] eqn: EQrsi; subst;
         [| erewrite pcm_op_unit in EQR by apply _; discriminate].
-        clear - HE HES EQrsi EQR.
-        assert (HH : rf · (Some r · s) = 0); [clear HES | rewrite HH in HES; contradiction].
-        eapply ores_equiv_eq; rewrite <- HE, comp_map_remove by eassumption.
+        clear - HE EQrsi EQR.
+        assert (HH : rf · (Some r · comp_map rs) = 0); [clear HE | rewrite HH in HE; contradiction].
+        eapply ores_equiv_eq; rewrite comp_map_remove by eassumption.
         rewrite (assoc (Some r)), (comm (Some r)), EQR, comm.
         erewrite !pcm_op_zero by apply _; reflexivity.
     Qed.
@@ -196,13 +192,13 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
     Proof.
       intros w' n r1 [Hpq Hqr] w HSub; specialize (Hpq _ HSub); rewrite HSub in Hqr; clear w' HSub.
       intros np rp HLe HS Hp w1; intros; specialize (Hpq _ _ HLe HS Hp).
-      edestruct Hpq as [w2 [rq [sq [HSw12 [Hq HEq] ] ] ] ]; try eassumption; [|].
+      edestruct Hpq as [w2 [rq [HSw12 [Hq HEq] ] ] ]; try eassumption; [|].
       { clear - HD HMS; intros j [Hmf Hm12]; apply (HD j); split; [assumption |].
         destruct Hm12 as [Hm1 | Hm2]; [left; assumption | apply HMS, Hm2].
       }
       clear HS; assert (HS : pcm_unit _ ⊑ rq) by (exists rq; now erewrite comm, pcm_op_unit by apply _).
       rewrite <- HLe, HSub in Hqr; specialize (Hqr _ HSw12); clear Hpq HE w HSub Hp.
-      edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [sR [HSw23 [Hr HEr] ] ] ] ];
+      edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [HSw23 [Hr HEr] ] ] ];
         try (reflexivity || eassumption); [now auto with arith | |].
       { clear - HD HMS; intros j [Hmf Hm23]; apply (HD j); split; [assumption |].
         destruct Hm23 as [Hm2 | Hm3]; [apply HMS, Hm2 | right; assumption].
@@ -216,7 +212,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
     Proof.
       intros w' n r1 Himp w HSub; rewrite HSub in Himp; clear w' HSub.
       intros np rp HLe HS Hp w1; intros.
-      exists w1 rp s; split; [reflexivity | split; [| assumption ] ].
+      exists w1 rp; split; [reflexivity | split; [| assumption ] ].
       eapply Himp; [assumption | now eauto with arith | exists rp; now erewrite comm, pcm_op_unit by apply _ |].
       unfold lt in HLe0; rewrite HLe0, <- HSub; assumption.
     Qed.
@@ -227,8 +223,8 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
       intros w' n r1 HVS w HSub; specialize (HVS _ HSub); clear w' r1 HSub.
       intros np rpr HLe _ [rp [rr [HR [Hp Hr] ] ] ] w'; intros.
       assert (HS : pcm_unit _ ⊑ rp) by (exists rp; now erewrite comm, pcm_op_unit by apply _).
-      specialize (HVS _ _ HLe HS Hp w' (Some rr · rf) s (mf ∪ mf0) σ k); clear HS.
-      destruct HVS as [w'' [rq [s' [HSub' [Hq HEq] ] ] ] ]; try assumption; [| |].
+      specialize (HVS _ _ HLe HS Hp w' (Some rr · rf) (mf ∪ mf0) σ k); clear HS.
+      destruct HVS as [w'' [rq [HSub' [Hq HEq] ] ] ]; try assumption; [| |].
       - (* disjointness of masks: possible lemma *)
         clear - HD HDisj; intros i [ [Hmf | Hmf] Hm12]; [eapply HDisj; now eauto |].
         eapply HD; split; [eassumption | tauto].
@@ -236,7 +232,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
         clear; intros i; tauto.
       - rewrite assoc in HEq; destruct (Some rq · Some rr) as [rqr |] eqn: HR';
         [| apply wsat_not_empty in HEq; [contradiction | now erewrite !pcm_op_zero by apply _] ].
-        exists w'' rqr s'; split; [assumption | split].
+        exists w'' rqr; split; [assumption | split].
         + unfold lt in HLe0; rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr.
           rewrite HR'; split; now auto.
         + eapply wsat_equiv, HEq; try reflexivity; [].
@@ -275,14 +271,15 @@ Qed.
     Proof.
       unfold ownLP; intros _ _ _ w _ n [rp' rl'] _ _ HG w'; intros.
       destruct rl as [rl |]; simpl in HG; [| contradiction].
+      destruct HE as [rs HE].
       destruct HG as [ [rdp rdl] EQr]; rewrite pcm_op_split in EQr; destruct EQr as [EQrp EQrl].
       erewrite comm, pcm_op_unit in EQrp by apply _; simpl in EQrp; subst rp'.
-      destruct (Some (rdp, rl') · rf · s) as [t |] eqn: EQt;
+      destruct (Some (rdp, rl') · rf · comp_map rs) as [t |] eqn: EQt;
         [| destruct HE as [HES _]; setoid_rewrite EQt in HES; contradiction].
-      assert (EQt' : Some (rdp, rl') · rf · s == Some t) by (rewrite EQt; reflexivity).
+      assert (EQt' : Some (rdp, rl') · rf · comp_map rs == Some t) by (rewrite EQt; reflexivity).
       clear EQt; rename EQt' into EQt.
       destruct rf as [ [rfp rfl] |]; [| now erewrite (comm _ 0), !pcm_op_zero in EQt by apply _].
-      destruct s as [ [sp sl] |]; [| now erewrite (comm _ 0), pcm_op_zero in EQt by apply _].
+      destruct (comp_map rs) as [ [sp sl] |] eqn:EQrs; [| now erewrite (comm _ 0), pcm_op_zero in EQt by apply _].
       destruct (Some (rdp, rl') · Some (rfp, rfl)) as [ [rdfp rdfl] |] eqn: EQdf;
         setoid_rewrite EQdf in EQt; [| now erewrite pcm_op_zero in EQt by apply _].
       destruct (HU (Some rdl · Some rfl · Some sl)) as [rsl [HPrsl HCrsl] ].
@@ -292,14 +289,15 @@ Qed.
         now rewrite <- EQdf, <- EQrl, (comm (Some rdl)), <- (assoc (Some rl)), <- assoc, HEq in EQt.
       - destruct (rsl · Some rdl) as [rsl' |] eqn: EQrsl;
         [| contradiction HCrsl; eapply ores_equiv_eq; now erewrite !assoc, EQrsl, !pcm_op_zero by apply _ ].
-        exists w' (rdp, rsl') (Some (sp, sl)); split; [reflexivity | split].
+        exists w' (rdp, rsl'); split; [reflexivity | split].
         + exists (exist _ rsl HPrsl); destruct rsl as [rsl |];
           [simpl | now erewrite pcm_op_zero in EQrsl by apply _].
           exists (rdp, rdl); rewrite pcm_op_split.
           split; [now erewrite comm, pcm_op_unit by apply _ | now rewrite comm, EQrsl].
-        + destruct HE as [HES HEL]; split; [| assumption]; clear HEL.
+        + destruct HE as [HES HEL]. exists rs. split; [| assumption]; clear HEL.
           assert (HT := ores_equiv_eq _ _ _ EQt); setoid_rewrite EQdf in HES;
           setoid_rewrite HT in HES; clear HT; destruct t as [tp tl].
+          rewrite EQrs; clear rs EQrs.
           destruct (rsl · (Some rdl · Some rfl · Some sl)) as [tl' |] eqn: EQtl;
           [| now contradiction HCrsl]; clear HCrsl.
           assert (HT : Some (rdp, rsl') · Some (rfp, rfl) · Some (sp, sl) = Some (tp, tl')); [| setoid_rewrite HT; apply HES].
@@ -366,19 +364,22 @@ Qed.
       { intros j; destruct (Peano_dec.eq_nat_dec i j); [subst j; rewrite HLi; exact I|].
         now rewrite fdUpdate_neq by assumption.
       }
-      exists (fdUpdate i (ı' p) w) (pcm_unit _) (Some r · s); split; [assumption | split].
+      exists (fdUpdate i (ı' p) w) (pcm_unit _); split; [assumption | split].
       - exists (exist _ i Hm); do 16 red.
         unfold proj1_sig; rewrite fdUpdate_eq; reflexivity.
       - erewrite pcm_op_unit by apply _.
-        assert (HR : rf · (Some r · s) = Some r · rf · s)
-          by (eapply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
-        destruct HE as [HES [rs [HE HM] ] ].
-        split; [setoid_rewrite HR; assumption | clear HR].
+        destruct HE as [rs [HE HM] ].
+        exists (fdUpdate i r rs).
         assert (HRi : rs i = None).
         { destruct (HM i) as [HDom _]; [tauto |].
           rewrite <- fdLookup_notin_strong, HDom, fdLookup_notin_strong; assumption.
         }
-        exists (fdUpdate i r rs); split; [now rewrite <- comp_map_insert_new, HE by assumption | intros j Hm'].
+        split.
+        {
+          rewrite <-comp_map_insert_new by assumption.
+          rewrite assoc, (comm rf). assumption.
+        }
+        intros j Hm'.
         rewrite !fdLookup_in_strong; destruct (Peano_dec.eq_nat_dec i j).
         + subst j; rewrite !fdUpdate_eq; split; [intuition now eauto | intros].
           simpl in HLw, HLrs; subst ri; rewrite <- HLw, isoR, <- HSub.
diff --git a/iris_wp.v b/iris_wp.v
index 8b8c265df7bae40a8db9789f44f26e42569afce3..c73e63b616daacad4e9c95967424a0836de8955f 100644
--- a/iris_wp.v
+++ b/iris_wp.v
@@ -27,20 +27,20 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
     Local Obligation Tactic := intros; eauto with typeclass_instances.
 
     Definition wpFP safe m (WP : expr -n> (value -n> Props) -n> Props) e φ w n r :=
-      forall w' k s rf mf σ (HSw : w ⊑ w') (HLt : k < n) (HD : mf # m)
-             (HE : wsat σ (m ∪ mf) (Some r · rf) s w' @ S k),
+      forall w' k rf mf σ (HSw : w ⊑ w') (HLt : k < n) (HD : mf # m)
+             (HE : wsat σ (m ∪ mf) (Some r · rf) w' @ S k),
         (forall (HV : is_value e),
-         exists w'' r' s', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
-                           /\ wsat σ (m ∪ mf) (Some r' · rf) s' w'' @ S k) /\
+         exists w'' r', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
+                           /\ wsat σ (m ∪ mf) (Some r' · rf) w'' @ S k) /\
         (forall σ' ei ei' K (HDec : e = K [[ ei ]])
                 (HStep : prim_step (ei, σ) (ei', σ')),
-         exists w'' r' s', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
-                           /\ wsat σ' (m ∪ mf) (Some r' · rf) s' w'' @ k) /\
+         exists w'' r', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
+                           /\ wsat σ' (m ∪ mf) (Some r' · rf) w'' @ k) /\
         (forall e' K (HDec : e = K [[ fork e' ]]),
-         exists w'' rfk rret s', w' ⊑ w''
+         exists w'' rfk rret, w' ⊑ w''
                                  /\ WP (K [[ fork_ret ]]) φ w'' k rret
                                  /\ WP e' (umconst ⊤) w'' k rfk
-                                 /\ wsat σ (m ∪ mf) (Some rfk · Some rret · rf) s' w'' @ k) /\
+                                 /\ wsat σ (m ∪ mf) (Some rfk · Some rret · rf) w'' @ k) /\
         (forall HSafe : safe = true,
          is_value e \/
          (exists σ' ei ei' K, e = K [[ ei ]] /\ prim_step (ei, σ) (ei', σ')) \/
@@ -49,30 +49,30 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
     Program Definition wpF safe m : (expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props :=
       n[(fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP safe m WP e φ w) _)])])])].
     Next Obligation.
-      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf mf σ HSw HLt HD HE.
+      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k rf mf σ HSw HLt HD HE.
       rewrite <- EQr, (comm (Some rd)), <- assoc in HE.
-      specialize (Hp w' k s (Some rd · rf) mf σ); destruct Hp as [HV [HS [HF HS' ] ] ];
+      specialize (Hp w' k (Some rd · rf) mf σ); destruct Hp as [HV [HS [HF HS' ] ] ];
       [| now eauto with arith | ..]; try assumption; [].      
       split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
-      - specialize (HV HV0); destruct HV as [w'' [r1' [s' [HSw' [Hφ HE'] ] ] ] ].
+      - specialize (HV HV0); destruct HV as [w'' [r1' [HSw' [Hφ HE'] ] ] ].
         rewrite assoc, (comm (Some r1')) in HE'.
         destruct (Some rd · Some r1') as [r2' |] eqn: HR;
           [| apply wsat_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
-        exists w'' r2' s'; split; [assumption | split; [| assumption] ].
+        exists w'' r2'; split; [assumption | split; [| assumption] ].
         eapply uni_pred, Hφ; [| eexists; rewrite <- HR]; reflexivity.
-      - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [s' [HSw' [HWP HE'] ] ] ] ].
+      - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
         rewrite assoc, (comm (Some r1')) in HE'.
-        destruct k as [| k]; [exists w'' r1' s'; simpl wsat; tauto |].
+        destruct k as [| k]; [exists w'' r1'; simpl wsat; tauto |].
         destruct (Some rd · Some r1') as [r2' |] eqn: HR;
           [| apply wsat_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
-        exists w'' r2' s'; split; [assumption | split; [| assumption] ].
+        exists w'' r2'; split; [assumption | split; [| assumption] ].
         eapply uni_pred, HWP; [| eexists; rewrite <- HR]; reflexivity.
-      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
-        destruct k as [| k]; [exists w'' rfk rret1 s'; simpl wsat; tauto |].
+      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [HSw' [HWR [HWF HE'] ] ] ] ] ].
+        destruct k as [| k]; [exists w'' rfk rret1; simpl wsat; tauto |].
         rewrite assoc, <- (assoc (Some rfk)), (comm (Some rret1)) in HE'.
         destruct (Some rd · Some rret1) as [rret2 |] eqn: HR;
           [| apply wsat_not_empty in HE'; [contradiction | now erewrite (comm _ 0), !pcm_op_zero by apply _] ].
-        exists w'' rfk rret2 s'; repeat (split; try assumption); [].
+        exists w'' rfk rret2; repeat (split; try assumption); [].
         eapply uni_pred, HWR; [| eexists; rewrite <- HR]; reflexivity.
       - auto.
     Qed.
@@ -88,22 +88,22 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         edestruct (Hp (extend w2' w1)) as [HV [HS [HF HS'] ] ]; try eassumption;
         [eapply wsat_dist, HE; [eassumption | now eauto with arith] |].
         split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
-        + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
+        + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
           assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
           assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r' s'; split; [assumption |].
+          exists (extend w1'' w2') r'; split; [assumption |].
           split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ].
           eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
-        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
+        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
           assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
           assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r' s'; split; [assumption |].
+          exists (extend w1'' w2') r'; split; [assumption |].
           split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ].
           eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
-        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
+        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
           assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
           assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') rfk rret s'; split; [assumption |].
+          exists (extend w1'' w2') rfk rret; split; [assumption |].
           split; [| split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ] ];
           eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
         + auto.
@@ -111,22 +111,22 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         edestruct (Hp (extend w2' w2)) as [HV [HS [HF HS'] ] ]; try eassumption;
         [eapply wsat_dist, HE; [eassumption | now eauto with arith] |].
         split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF] ] ]; intros.
-        + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
+        + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
           assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
           assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r' s'; split; [assumption |].
+          exists (extend w1'' w2') r'; split; [assumption |].
           split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ].
           eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
-        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
+        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
           assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
           assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r' s'; split; [assumption |].
+          exists (extend w1'' w2') r'; split; [assumption |].
           split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ].
           eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
-        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
+        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
           assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
           assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') rfk rret s'; split; [assumption |].
+          exists (extend w1'' w2') rfk rret; split; [assumption |].
           split; [| split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ] ];
           eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
         + auto.
@@ -143,25 +143,25 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
       split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
       - split; [| split; [| split] ]; intros.
-        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
-          exists w'' r' s'; split; [assumption | split; [| assumption] ].
+        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
           apply EQφ, Hφ; now eauto with arith.
-        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
-          exists w'' r' s'; split; [assumption | split; [| assumption] ].
+        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
           eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | now eauto with arith].
-        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
-          exists w'' rfk rret s'; repeat (split; try assumption); [].
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+          exists w'' rfk rret ; repeat (split; try assumption); [].
           eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | now eauto with arith].
         + auto.
       - split; [| split; [| split] ]; intros.
-        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
-          exists w'' r' s'; split; [assumption | split; [| assumption] ].
+        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
           apply EQφ, Hφ; now eauto with arith.
-        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
-          exists w'' r' s'; split; [assumption | split; [| assumption] ].
+        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
           eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | now eauto with arith].
-        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
-          exists w'' rfk rret s'; repeat (split; try assumption); [].
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+          exists w'' rfk rret; repeat (split; try assumption); [].
           eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | now eauto with arith].
         + auto.
     Qed.
@@ -181,19 +181,19 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       intros WP1 WP2 EQWP e φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
       split; intros Hp w'; intros; edestruct Hp as [HF [HS [HV HS'] ] ]; try eassumption; [|].
       - split; [assumption | split; [| split]; intros].
-        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
-          exists w'' r' s'; split; [assumption | split; [| assumption] ].
+        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
           eapply (EQWP _ _ _), HWP; now eauto with arith.
-        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
-          exists w'' rfk rret s'; split; [assumption |].
+        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+          exists w'' rfk rret; split; [assumption |].
           split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
         + auto.
       - split; [assumption | split; [| split]; intros].
-        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
-          exists w'' r' s'; split; [assumption | split; [| assumption] ].
+        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
           eapply (EQWP _ _ _), HWP; now eauto with arith.
-        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
-          exists w'' rfk rret s'; split; [assumption |].
+        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+          exists w'' rfk rret; split; [assumption |].
           split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
         + auto.
     Qed.
@@ -203,19 +203,19 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       intros n WP1 WP2 EQWP e φ w k r HLt.
       split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
       - split; [assumption | split; [| split]; intros].
-        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
-          exists w'' r' s'; split; [assumption | split; [| assumption] ].
+        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
           eapply EQWP, HWP; now eauto with arith.
-        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
-          exists w'' rfk rret s'; split; [assumption |].
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+          exists w'' rfk rret; split; [assumption |].
           split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
         + auto.
       - split; [assumption | split; [| split]; intros].
-        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
-          exists w'' r' s'; split; [assumption | split; [| assumption] ].
+        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
           eapply EQWP, HWP; now eauto with arith.
-        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
-          exists w'' rfk rret s'; split; [assumption |].
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+          exists w'' rfk rret; split; [assumption |].
           split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
         + auto.
     Qed.
@@ -295,29 +295,28 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       unfold wp; apply fixp_eq.
     Qed.
 
-    Lemma adequate_tp safe m n k e e' tp tp' σ σ' φ w r rs s
+    Lemma adequate_tp safe m n k e e' tp tp' σ σ' φ w r rs
           (HSN  : stepn n (e :: tp, σ) (e' :: tp', σ'))
           (HV   : is_value e')
           (HWE  : wp safe m e φ w (n + S k) r)
           (HWTP : wptp safe m w (n + S k) tp rs)
-          (HE   : wsat σ m (Some r · comp_list rs) s w @ n + S k) :
-      exists w' r' s',
-        w ⊑ w' /\ φ (exist _ e' HV) w' (S k) r' /\ wsat σ' m (Some r') s' w' @ S k.
+          (HE   : wsat σ m (Some r · comp_list rs) w @ n + S k) :
+      exists w' r',
+        w ⊑ w' /\ φ (exist _ e' HV) w' (S k) r' /\ wsat σ' m (Some r') w' @ S k.
     Proof.
-      revert e tp σ w r rs s HSN HWE HWTP HE; induction n using wf_nat_ind; rename H into HInd.
+      revert e tp σ w r rs HSN HWE HWTP HE; induction n using wf_nat_ind; rename H into HInd.
       intros; inversion HSN; subst; clear HSN.
       (* e is a value *)
       { rename e' into e; clear HInd HWTP; simpl plus in *; rewrite unfold_wp in HWE.
         edestruct (HWE w k) as [HVal _];
           [reflexivity | unfold lt; reflexivity | apply mask_emp_disjoint
            | rewrite mask_emp_union; eassumption |].
-        specialize (HVal HV); destruct HVal as [w' [r' [s' [HSW [Hφ HE'] ] ] ] ].
+        specialize (HVal HV); destruct HVal as [w' [r' [HSW [Hφ HE'] ] ] ].
         rewrite mask_emp_union in HE'; destruct (Some r' · comp_list rs) as [r'' |] eqn: EQr.
-        - exists w' r'' s'; split; [assumption | split; [| assumption] ].
+        - exists w' r''; split; [assumption | split; [| assumption] ].
           eapply uni_pred, Hφ; [reflexivity |].
           rewrite ord_res_optRes; exists (comp_list rs); rewrite comm, EQr; reflexivity.
-        - exfalso; eapply wsat_not_empty, HE'.
-          now erewrite pcm_op_zero by apply _.
+        - exfalso; eapply wsat_not_empty, HE'. reflexivity.
       }
       rename n0 into n; specialize (HInd n (le_n _)); inversion HS; subst; clear HS.
       (* atomic step *)
@@ -325,19 +324,19 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         (* step in e *)
         - simpl in HSN0; rewrite unfold_wp in HWE; edestruct (HWE w (n + S k)) as [_ [HS _] ];
           [reflexivity | apply le_n | apply mask_emp_disjoint | rewrite mask_emp_union; eassumption |].
-          edestruct HS as [w' [r' [s' [HSW [HWE' HE'] ] ] ] ]; [reflexivity | eassumption | clear HS HWE HE].
+          edestruct HS as [w' [r' [HSW [HWE' HE'] ] ] ]; [reflexivity | eassumption | clear HS HWE HE].
           rewrite mask_emp_union in HE'; setoid_rewrite HSW; eapply HInd; try eassumption.
           eapply wptp_closure, HWTP; [assumption | now auto with arith].
         (* step in a spawned thread *)
         - apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [EQrs [HWTP1 HWTP2] ] ] ].
           inversion HWTP2; subst; clear HWTP2; rewrite unfold_wp in WPE.
-          edestruct (WPE w (n + S k) s (Some r · comp_list (rs1 ++ rs0))) as [_ [HS _] ];
+          edestruct (WPE w (n + S k) (Some r · comp_list (rs1 ++ rs0))) as [_ [HS _] ];
             [reflexivity | apply le_n | apply mask_emp_disjoint
              | eapply wsat_equiv, HE; try reflexivity; [apply mask_emp_union |] |].
           + rewrite !comp_list_app; simpl comp_list; unfold equiv.
             rewrite assoc, (comm (Some r0)), <- assoc; apply pcm_op_equiv; [reflexivity |].
             now rewrite assoc, (comm (Some r0)), <- assoc.
-          + edestruct HS as [w' [r0' [s' [HSW [WPE' HE'] ] ] ] ];
+          + edestruct HS as [w' [r0' [HSW [WPE' HE'] ] ] ];
             [reflexivity | eassumption | clear WPE HS].
             setoid_rewrite HSW; eapply HInd; try eassumption; [| |].
             * rewrite <- HSW; eapply uni_pred, HWE; [now auto with arith | reflexivity].
@@ -353,7 +352,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       (* fork from e *)
       - simpl in HSN0; rewrite unfold_wp in HWE; edestruct (HWE w (n + S k)) as [_ [_ [HF _] ] ];
         [reflexivity | apply le_n | apply mask_emp_disjoint | rewrite mask_emp_union; eassumption |].
-        specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [s' [HSW [HWE' [HWFK HE'] ] ] ] ] ] ].
+        specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [HSW [HWE' [HWFK HE'] ] ] ] ] ].
         clear HWE HE; setoid_rewrite HSW; eapply HInd with (rs := rs ++ [rfk]); try eassumption; [|].
         + apply wptp_app; [| now auto using wptp].
           eapply wptp_closure, HWTP; [assumption | now auto with arith].
@@ -364,12 +363,12 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       (* fork from a spawned thread *)
       - apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [EQrs [HWTP1 HWTP2] ] ] ].
         inversion HWTP2; subst; clear HWTP2; rewrite unfold_wp in WPE.
-        edestruct (WPE w (n + S k) s (Some r · comp_list (rs1 ++ rs0))) as [_ [_ [HF _] ] ];
+        edestruct (WPE w (n + S k) (Some r · comp_list (rs1 ++ rs0))) as [_ [_ [HF _] ] ];
           [reflexivity | apply le_n | apply mask_emp_disjoint
            | eapply wsat_equiv, HE; try reflexivity; [apply mask_emp_union |] |].
         + rewrite assoc, (comm (Some r0)), <- assoc; apply pcm_op_equiv; [reflexivity |].
           rewrite !comp_list_app; simpl comp_list; now rewrite assoc, (comm (Some r0)), <- assoc.
-        + specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [s' [HSW [WPE' [WPS HE'] ] ] ] ] ] ]; clear WPE.
+        + specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [HSW [WPE' [WPS HE'] ] ] ] ] ]; clear WPE.
           setoid_rewrite HSW; eapply HInd; try eassumption; [| |].
           * rewrite <- HSW; eapply uni_pred, HWE; [now auto with arith | reflexivity].
           * apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
@@ -394,14 +393,14 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
     (** This is a (relatively) generic adequacy statement for all postconditions; one can
         simplify it for certain classes of assertions (e.g.,
         independent of the worlds) and obtain easy corollaries. *)
-    Theorem adequacy_post safe m e p φ n k e' tp σ σ' w r s
+    Theorem adequacy_post safe m e p φ n k e' tp σ σ' w r
             (HT  : valid (ht safe m p e φ))
             (HSN : stepn n ([e], σ) (e' :: tp, σ'))
             (HV  : is_value e')
             (HP  : p w (n + S k) r)
-            (HE  : wsat σ m (Some r) s w @ n + S k) :
-      exists w' r' s',
-        w ⊑ w' /\ φ (exist _ e' HV) w' (S k) r' /\ wsat σ' m (Some r') s' w' @ S k.
+            (HE  : wsat σ m (Some r) w @ n + S k) :
+      exists w' r',
+        w ⊑ w' /\ φ (exist _ e' HV) w' (S k) r' /\ wsat σ' m (Some r') w' @ S k.
     Proof.
       specialize (HT w (n + S k) r).
       eapply adequate_tp; [eassumption | | constructor | eapply wsat_equiv, HE; try reflexivity; [] ].
@@ -430,14 +429,13 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
             (HV : is_value e') :
         φ (exist _ e' HV).
     Proof.
-      edestruct (adequacy_post _ _ _ _ _ _ 0 _ _ _ _ fdEmpty (ex_own _ σ, pcm_unit _) 1 HT HSN) as [w [r [s [H_wle [H_phi _] ] ] ] ].
+      edestruct (adequacy_post _ _ _ _ _ _ 0 _ _ _ _ fdEmpty (ex_own _ σ, pcm_unit _) HT HSN) as [w [r [H_wle [H_phi _] ] ] ].
       - exists (pcm_unit _); now rewrite pcm_op_unit by apply _.
-      - rewrite Plus.plus_comm; split.
+      - hnf. rewrite Plus.plus_comm. exists (fdEmpty (V:=res)). split.
         + assert (HS : Some (ex_own _ σ, pcm_unit _) · 1 = Some (ex_own _ σ, pcm_unit _));
           [| now setoid_rewrite HS].
           eapply ores_equiv_eq; now erewrite comm, pcm_op_unit by apply _.
-        + exists (fdEmpty (V:=res)); split; [reflexivity|].
-          intros i _; split; [reflexivity |].
+        + intros i _; split; [reflexivity |].
           intros _ _ [].
       - exact H_phi.
     Qed.
@@ -470,7 +468,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
     Proof.
       intros w' nn rr w _ n r' _ _ _; clear w' nn rr.
       rewrite unfold_wp; intros w'; intros; split; [| split; [| split] ]; intros.
-      - exists w' r' s; split; [reflexivity | split; [| assumption] ].
+      - exists w' r'; split; [reflexivity | split; [| assumption] ].
         simpl; reflexivity.
       - contradiction (values_stuck _ HV _ _ HDec).
         repeat eexists; eassumption.
@@ -515,7 +513,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       rewrite unfold_wp in He; rewrite unfold_wp.
       destruct (is_value_dec e) as [HVal | HNVal]; [clear IH |].
       - intros w'; intros; edestruct He as [HV _]; try eassumption; [].
-        clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [s' [HSw' [Hφ HE] ] ] ] ].
+        clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [Hφ HE] ] ] ].
         (* Fold the goal back into a wp *)
         setoid_rewrite HSw'.
         assert (HT : wp safe m (K [[ e ]]) φ' w'' (S k) r');
@@ -529,16 +527,16 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         + clear He HF HE; edestruct step_by_value as [K' EQK];
           [eassumption | repeat eexists; eassumption | eassumption |].
           subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
-          edestruct HS as [w'' [r' [s' [HSw' [He HE] ] ] ] ]; try eassumption; [].
+          edestruct HS as [w'' [r' [HSw' [He HE] ] ] ]; try eassumption; [].
           subst e; clear HStep HS.
-          do 3 eexists; split; [eassumption | split; [| eassumption] ].
+          do 2 eexists; split; [eassumption | split; [| eassumption] ].
           rewrite <- fill_comp; apply IH; try assumption; [].
           unfold lt in HLt; rewrite <- HSw', <- HSw, Le.le_n_Sn, HLt; apply HK.
         + clear He HS HE; edestruct fork_by_value as [K' EQK]; try eassumption; [].
           subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
-          edestruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE] ] ] ] ] ] ];
+          edestruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE] ] ] ] ] ];
             try eassumption; []; subst e; clear HF.
-          do 4 eexists; split; [eassumption | split; [| split; eassumption] ].
+          do 3 eexists; split; [eassumption | split; [| split; eassumption] ].
           rewrite <- fill_comp; apply IH; try assumption; [].
           unfold lt in HLt; rewrite <- HSw', <- HSw, Le.le_n_Sn, HLt; apply HK.
         + clear IH He HS HE HF; specialize (HS' HSafe); clear HSafe.
@@ -572,7 +570,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       intros wz nz rz [ [HP He] Hφ] w HSw n r HLe _ Hp.
       specialize (HP _ HSw _ _ HLe (unit_min _) Hp); rewrite unfold_wp.
       rewrite <- HLe, HSw in He, Hφ; clear wz nz HSw HLe Hp.
-      intros w'; intros; edestruct HP as [w'' [r' [s' [HSw' [Hp' HE'] ] ] ] ]; try eassumption; [now rewrite mask_union_idem |].
+      intros w'; intros; edestruct HP as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [now rewrite mask_union_idem |].
       clear HP HE; rewrite HSw in He; specialize (He w'' HSw' _ r' HLt (unit_min _) Hp').
       setoid_rewrite HSw'.
       assert (HT : wp safe m e φ w'' (S k) r');
@@ -585,18 +583,18 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       rename H into IH; intros; rewrite unfold_wp; rewrite unfold_wp in He.
       intros w'; intros; edestruct He as [HV [HS [HF HS'] ] ]; try eassumption; [].
       split; [intros HVal; clear HS HF IH HS' | split; intros; [clear HV HF HS' | split; [intros; clear HV HS HS' | clear HV HS HF ] ] ].
-      - clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [s' [HSw' [Hφ' HE] ] ] ] ].
+      - clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [Hφ' HE] ] ] ].
         eapply Hφ in Hφ'; [| etransitivity; eassumption | apply HLt | apply unit_min].
-        clear w n HSw Hφ HLt; edestruct Hφ' as [w [r'' [s'' [HSw [Hφ HE'] ] ] ] ];
+        clear w n HSw Hφ HLt; edestruct Hφ' as [w [r'' [HSw [Hφ HE'] ] ] ];
         [reflexivity | apply le_n | rewrite mask_union_idem; eassumption | eassumption |].
-        exists w r'' s''; split; [etransitivity; eassumption | split; assumption].
-      - clear HE He; edestruct HS as [w'' [r' [s' [HSw' [He HE] ] ] ] ];
+        exists w r''; split; [etransitivity; eassumption | split; assumption].
+      - clear HE He; edestruct HS as [w'' [r' [HSw' [He HE] ] ] ];
         try eassumption; clear HS.
-        do 3 eexists; split; [eassumption | split; [| eassumption] ].
+        do 2 eexists; split; [eassumption | split; [| eassumption] ].
         apply IH; try assumption; [].
         unfold lt in HLt; rewrite Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
-      - clear HE He; edestruct HF as [w'' [rfk [rret [s' [HSw' [HWF [HWR HE] ] ] ] ] ] ]; [eassumption |].
-        clear HF; do 4 eexists; split; [eassumption | split; [| split; eassumption] ].
+      - clear HE He; edestruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ]; [eassumption |].
+        clear HF; do 3 eexists; split; [eassumption | split; [| split; eassumption] ].
         apply IH; try assumption; [].
         unfold lt in HLt; rewrite Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
       - assumption.
@@ -610,7 +608,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       intros wz nz rz [ [HP He] Hφ] w HSw n r HLe _ Hp.
       specialize (HP _ HSw _ _ HLe (unit_min _) Hp); rewrite unfold_wp.
       split; [intros HV; contradiction (atomic_not_value e) |].
-      edestruct HP as [w'' [r' [s' [HSw' [Hp' HE'] ] ] ] ]; try eassumption; [|]; clear HP.
+      edestruct HP as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [|]; clear HP.
       { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
         destruct Hmm'; [| apply HSub]; assumption.
       }
@@ -620,8 +618,8 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         unfold lt in HLt; rewrite HSw0, <- HLt in Hφ; clear w n HSw0 HLt Hp'.
         rewrite unfold_wp in He; edestruct He as [_ [HS _] ];
           [reflexivity | apply le_n | rewrite HSub; eassumption | eassumption |].
-        edestruct HS as [w [r'' [s'' [HSw [He' HE] ] ] ] ]; try eassumption; clear He HS HE'.
-        destruct k as [| k]; [exists w' r' s'; split; [reflexivity | split; [apply wpO | exact I] ] |].
+        edestruct HS as [w [r'' [HSw [He' HE] ] ] ]; try eassumption; clear He HS HE'.
+        destruct k as [| k]; [exists w' r'; split; [reflexivity | split; [apply wpO | exact I] ] |].
         assert (HNV : ~ is_value ei)
           by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
         subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
@@ -631,17 +629,17 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         rewrite HSw', HSw in Hφ; clear - HE He' Hφ HSub HVal HD.
         rewrite unfold_wp in He'; edestruct He' as [HV _];
         [reflexivity | apply le_n | rewrite HSub; eassumption | eassumption |].
-        clear HE He'; specialize (HV HVal); destruct HV as [w' [r [s [HSw [Hφ' HE] ] ] ] ].
+        clear HE He'; specialize (HV HVal); destruct HV as [w' [r [HSw [Hφ' HE] ] ] ].
         eapply Hφ in Hφ'; [| assumption | apply Le.le_n_Sn | apply unit_min].
-        clear Hφ; edestruct Hφ' as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ];
+        clear Hφ; edestruct Hφ' as [w'' [r' [HSw' [Hφ HE'] ] ] ];
           [reflexivity | apply le_n | | eassumption |].
         { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
           destruct Hmm'; [apply HSub |]; assumption.
         }
-        clear Hφ' HE; exists w'' r' s'; split;
+        clear Hφ' HE; exists w'' r'; split;
         [etransitivity; eassumption | split; [| eassumption] ].
         clear - Hφ; rewrite unfold_wp; intros w; intros; split; [intros HVal' | split; intros; [intros; exfalso|split; [intros |] ] ].
-        + do 3 eexists; split; [reflexivity | split; [| eassumption] ].
+        + do 2 eexists; split; [reflexivity | split; [| eassumption] ].
           unfold lt in HLt; rewrite HLt, <- HSw.
           eapply φ, Hφ; [| apply le_n]; simpl; reflexivity.
         + eapply values_stuck; [.. | repeat eexists]; eassumption.
@@ -670,16 +668,16 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       { clear; intros j; tauto.
       }
       clear HW HE; split; [intros HVal; clear HS HF HInd | split; [intros; clear HV HF | split; [intros; clear HV HS | intros; clear HV HS HF] ] ].
-      - specialize (HV HVal); destruct HV as [w'' [r' [s' [HSW [Hφ HE] ] ] ] ].
-        do 3 eexists; split; [eassumption | split; [eassumption |] ].
+      - specialize (HV HVal); destruct HV as [w'' [r' [HSW [Hφ HE] ] ] ].
+        do 2 eexists; split; [eassumption | split; [eassumption |] ].
         eapply wsat_equiv, HE; try reflexivity; [].
         intros j; tauto.
-      - edestruct HS as [w'' [r' [s' [HSW [HW HE] ] ] ] ]; try eassumption; []; clear HS.
-        do 3 eexists; split; [eassumption | split; [eapply HInd, HW; assumption |] ].
+      - edestruct HS as [w'' [r' [HSW [HW HE] ] ] ]; try eassumption; []; clear HS.
+        do 2 eexists; split; [eassumption | split; [eapply HInd, HW; assumption |] ].
         eapply wsat_equiv, HE; try reflexivity; [].
         intros j; tauto.
-      - destruct (HF _ _ HDec) as [w'' [rfk [rret [s' [HSW [HWR [HWF HE] ] ] ] ] ] ]; clear HF.
-        do 4 eexists; split; [eassumption |].
+      - destruct (HF _ _ HDec) as [w'' [rfk [rret [HSW [HWR [HWF HE] ] ] ] ] ]; clear HF.
+        do 3 eexists; split; [eassumption |].
         do 2 (split; [apply HInd; eassumption |]).
         eapply wsat_equiv, HE; try reflexivity; [].
         intros j; tauto.
@@ -697,24 +695,24 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       rewrite unfold_wp; rewrite unfold_wp in He; intros w'; intros.
       rewrite <- EQr, <- assoc in HE; edestruct He as [HV [HS [HF HS'] ] ]; try eassumption; [].
       clear He; split; [intros HVal; clear HS HF IH HE | split; [clear HV HF HE | clear HV HS HE; split; [clear HS' | clear HF] ]; intros ].
-      - specialize (HV HVal); destruct HV as [w'' [r1' [s' [HSw' [Hφ HE] ] ] ] ].
+      - specialize (HV HVal); destruct HV as [w'' [r1' [HSw' [Hφ HE] ] ] ].
         rewrite assoc in HE; destruct (Some r1' · Some r2) as [r' |] eqn: EQr';
         [| eapply wsat_not_empty in HE; [contradiction | now erewrite !pcm_op_zero by apply _] ].
-        do 3 eexists; split; [eassumption | split; [| eassumption ] ].
+        do 2 eexists; split; [eassumption | split; [| eassumption ] ].
         exists r1' r2; split; [now rewrite EQr' | split; [assumption |] ].
         unfold lt in HLt; rewrite HLt, <- HSw', <- HSw; apply HLR.
-      - edestruct HS as [w'' [r1' [s' [HSw' [He HE] ] ] ] ]; try eassumption; []; clear HS.
-        destruct k as [| k]; [exists w' r1' s'; split; [reflexivity | split; [apply wpO | exact I] ] |].
+      - edestruct HS as [w'' [r1' [HSw' [He HE] ] ] ]; try eassumption; []; clear HS.
+        destruct k as [| k]; [exists w' r1'; split; [reflexivity | split; [apply wpO | exact I] ] |].
         rewrite assoc in HE; destruct (Some r1' · Some r2) as [r' |] eqn: EQr';
         [| eapply wsat_not_empty in HE; [contradiction | now erewrite !pcm_op_zero by apply _] ].
-        do 3 eexists; split; [eassumption | split; [| eassumption] ].
+        do 2 eexists; split; [eassumption | split; [| eassumption] ].
         eapply IH; try eassumption; [rewrite <- EQr'; reflexivity |].
         unfold lt in HLt; rewrite Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
-      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWF [HWR HE] ] ] ] ] ] ].
-        destruct k as [| k]; [exists w' rfk rret s'; split; [reflexivity | split; [apply wpO | split; [apply wpO | exact I] ] ] |].
+      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ].
+        destruct k as [| k]; [exists w' rfk rret; split; [reflexivity | split; [apply wpO | split; [apply wpO | exact I] ] ] |].
         rewrite assoc, <- (assoc (Some rfk)) in HE; destruct (Some rret · Some r2) as [rret' |] eqn: EQrret;
         [| eapply wsat_not_empty in HE; [contradiction | now erewrite (comm _ 0), !pcm_op_zero by apply _] ].
-        do 4 eexists; split; [eassumption | split; [| split; eassumption] ].
+        do 3 eexists; split; [eassumption | split; [| split; eassumption] ].
         eapply IH; try eassumption; [rewrite <- EQrret; reflexivity |].
         unfold lt in HLt; rewrite Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
       - auto.
@@ -732,15 +730,15 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       split; [intros; exfalso | split; intros; [| split; intros; [exfalso| ] ] ].
       - contradiction (atomic_not_value e).
       - destruct k as [| k];
-        [exists w' r s; split; [reflexivity | split; [apply wpO | exact I] ] |].
+        [exists w' r; split; [reflexivity | split; [apply wpO | exact I] ] |].
         rewrite unfold_wp in He; rewrite <- EQr, <- assoc in HE.
         edestruct He as [_ [HeS _] ]; try eassumption; [].
-        edestruct HeS as [w'' [r1' [s' [HSw' [He' HE'] ] ] ] ]; try eassumption; [].
+        edestruct HeS as [w'' [r1' [HSw' [He' HE'] ] ] ]; try eassumption; [].
         clear HE He HeS; rewrite assoc in HE'.
         destruct (Some r1' · Some r2) as [r' |] eqn: EQr';
           [| eapply wsat_not_empty in HE';
              [contradiction | now erewrite !pcm_op_zero by apply _] ].
-        do 3 eexists; split; [eassumption | split; [| eassumption] ].
+        do 2 eexists; split; [eassumption | split; [| eassumption] ].
         assert (HNV : ~ is_value ei)
           by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
         subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
@@ -750,11 +748,11 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         clear - He' HVal EQr' HLR; rename w'' into w; rewrite unfold_wp; intros w'; intros.
         split; [intros HV; clear HVal | split; intros; [exfalso| split; intros; [exfalso |] ] ].
         + rewrite unfold_wp in He'; rewrite <- EQr', <- assoc in HE; edestruct He' as [HVal _]; try eassumption; [].
-          specialize (HVal HV); destruct HVal as [w'' [r1'' [s'' [HSw' [Hφ HE'] ] ] ] ].
+          specialize (HVal HV); destruct HVal as [w'' [r1'' [HSw' [Hφ HE'] ] ] ].
           rewrite assoc in HE'; destruct (Some r1'' · Some r2) as [r'' |] eqn: EQr'';
           [| eapply wsat_not_empty in HE';
              [contradiction | now erewrite !pcm_op_zero by apply _] ].
-          do 3 eexists; split; [eassumption | split; [| eassumption] ].
+          do 2 eexists; split; [eassumption | split; [| eassumption] ].
           exists r1'' r2; split; [now rewrite EQr'' | split; [assumption |] ].
           unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; apply HLR.
         + eapply values_stuck; [.. | repeat eexists]; eassumption.
@@ -764,7 +762,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         + auto.
       - subst; eapply fork_not_atomic; eassumption.
       - rewrite <- EQr, <- assoc in HE; rewrite unfold_wp in He.
-        specialize (He w' k s (Some r2 · rf) mf σ HSw HLt HD0 HE); clear HE.
+        specialize (He w' k (Some r2 · rf) mf σ HSw HLt HD0 HE); clear HE.
         destruct He as [_ [_ [_ HS'] ] ]; auto.
     Qed.
 
@@ -784,10 +782,10 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         apply fork_inj in HDec; subst e'; rewrite <- EQr in HE.
         unfold lt in HLt; rewrite <- (le_S_n _ _ HLt), HSw in He.
         simpl in HLR; rewrite <- Le.le_n_Sn in HE.
-        do 4 eexists; split; [reflexivity | split; [| split; eassumption] ].
+        do 3 eexists; split; [reflexivity | split; [| split; eassumption] ].
         rewrite fill_empty; rewrite unfold_wp; rewrite <- (le_S_n _ _ HLt), HSw in HLR.
         clear - HLR; intros w''; intros; split; [intros | split; intros; [exfalso | split; intros; [exfalso |] ] ].
-        + do 3 eexists; split; [reflexivity | split; [| eassumption] ].
+        + do 2 eexists; split; [reflexivity | split; [| eassumption] ].
           exists (pcm_unit _) r2; split; [now erewrite pcm_op_unit by apply _ |].
           split; [| unfold lt in HLt; rewrite <- HLt, HSw in HLR; apply HLR].
           simpl; reflexivity.