diff --git a/iris_core.v b/iris_core.v
index 6d2a8e2d21dbf17f1f6fc2879b0e25a0285f98af..f5d92bbfa4a1a041c699628e0104a590bf65887f 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -1,4 +1,4 @@
-Require Import world_prop core_lang lang masks.
+Require Import world_prop core_lang masks.
 Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
 Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T.
@@ -10,7 +10,7 @@ Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T.
 End IrisRes.
   
 Module IrisCore (RL : PCM_T) (C : CORE_LANG).
-  Module Export L  := Lang C.
+  Export C.
   Module Export R  := IrisRes RL C.
   Module Export WP := WorldProp R.
 
@@ -310,6 +310,13 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
         | (x :: xs)%list => Some x · comp_list xs
       end.
 
+    Lemma comp_list_app rs1 rs2 :
+      comp_list (rs1 ++ rs2) == comp_list rs1 · comp_list rs2.
+    Proof.
+      induction rs1; simpl comp_list; [now rewrite pcm_op_unit by apply _ |].
+      now rewrite IHrs1, assoc.
+    Qed.
+
     Definition cod (m : nat -f> res) : list res := List.map snd (findom_t m).
     Definition comp_map (m : nat -f> res) : option res := comp_list (cod m).
 
diff --git a/iris_wp.v b/iris_wp.v
index c73e63b616daacad4e9c95967424a0836de8955f..33e6bc115a336f6e3e7c6fc0b76b4b61ed633c39 100644
--- a/iris_wp.v
+++ b/iris_wp.v
@@ -1,7 +1,9 @@
-Require Import world_prop core_lang masks iris_vs.
+Require Import ssreflect.
+Require Import world_prop core_lang lang masks iris_vs.
 Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
 Module IrisWP (RL : PCM_T) (C : CORE_LANG).
+  Module Export L  := Lang C.
   Module Export VS := IrisVS RL C.
 
   Delimit Scope iris_scope with iris.
@@ -22,11 +24,17 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       intros σ σc HC; apply HC.
     Qed.
 
-    Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : value -n> Props) (r : res).
+    (* We use this type quite a bit, so give it and its instances names *)
+    Definition vPred := value -n> Props.
+    Global Instance vPred_type  : Setoid vPred  := _.
+    Global Instance vPred_metr  : metric vPred  := _.
+    Global Instance vPred_cmetr : cmetric vPred := _.
+
+    Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : vPred) (r : res).
 
     Local Obligation Tactic := intros; eauto with typeclass_instances.
 
-    Definition wpFP safe m (WP : expr -n> (value -n> Props) -n> Props) e φ w n r :=
+    Definition wpFP safe m (WP : expr -n> vPred -n> Props) e φ w n r :=
       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),
@@ -46,7 +54,8 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
          (exists σ' ei ei' K, e = K [[ ei ]] /\ prim_step (ei, σ) (ei', σ')) \/
          (exists e' K, e = K [[ fork e' ]])).
 
-    Program Definition wpF safe m : (expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props :=
+    (* Define the function wp will be a fixed-point of *)
+    Program Definition wpF safe m : (expr -n> vPred -n> Props) -n> (expr -n> vPred -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 rf mf σ HSw HLt HD HE.
@@ -55,13 +64,13 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       [| 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' [HSw' [Hφ HE'] ] ] ].
-        rewrite assoc, (comm (Some r1')) in 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'; split; [assumption | split; [| assumption] ].
         eapply uni_pred, Hφ; [| eexists; rewrite <- HR]; reflexivity.
       - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
-        rewrite assoc, (comm (Some r1')) in HE'.
+        rewrite ->assoc, (comm (Some r1')) in HE'.
         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 _] ].
@@ -69,7 +78,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         eapply uni_pred, HWP; [| eexists; rewrite <- HR]; reflexivity.
       - 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'.
+        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; repeat (split; try assumption); [].
@@ -220,7 +229,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         + auto.
     Qed.
 
-    Definition wp safe m : expr -n> (value -n> Props) -n> Props :=
+    Definition wp safe m : expr -n> vPred -n> Props :=
       fixp (wpF safe m) (umconst (umconst ⊤)).
 
     Definition ht safe m P e φ := □ (P → wp safe m e φ).
@@ -234,53 +243,39 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
     Local Open Scope lang_scope.
     Local Open Scope list_scope.
 
-    Inductive stepn : nat -> cfg -> cfg -> Prop :=
-    | stepn_O ρ : stepn O ρ ρ
-    | stepn_S ρ1 ρ2 ρ3 n
-              (HS  : step ρ1 ρ2)
-              (HSN : stepn n ρ2 ρ3) :
-        stepn (S n) ρ1 ρ3.
-
     (* weakest-pre for a threadpool *)
-    Inductive wptp (safe : bool) (m : mask) (w : Wld) (n : nat) : tpool -> list res -> Prop :=
-    | wp_emp : wptp safe m w n nil nil
-    | wp_cons e r tp rs
-              (WPE  : wp safe m e (umconst ⊤) w n r)
-              (WPTP : wptp safe m w n tp rs) :
-        wptp safe m w n (e :: tp) (r :: rs).
+    Inductive wptp (safe : bool) (m : mask) (w : Wld) (n : nat) : tpool -> list res -> list vPred -> Prop :=
+    | wp_emp : wptp safe m w n nil nil nil
+    | wp_cons e φ r tp rs φs
+              (WPE  : wp safe m e φ w n r)
+              (WPTP : wptp safe m w n tp rs φs) :
+        wptp safe m w n (e :: tp) (r :: rs) (φ :: φs).
 
     (* Trivial lemmas about split over append *)
-    Lemma wptp_app safe m w n tp1 tp2 rs1 rs2
-          (HW1 : wptp safe m w n tp1 rs1)
-          (HW2 : wptp safe m w n tp2 rs2) :
-      wptp safe m w n (tp1 ++ tp2) (rs1 ++ rs2).
+    Lemma wptp_app safe m w n tp1 tp2 rs1 rs2 φs1 φs2
+          (HW1 : wptp safe m w n tp1 rs1 φs1)
+          (HW2 : wptp safe m w n tp2 rs2 φs2) :
+      wptp safe m w n (tp1 ++ tp2) (rs1 ++ rs2) (φs1 ++ φs2).
     Proof.
       induction HW1; [| constructor]; now trivial.
     Qed.
 
-    Lemma wptp_app_tp safe m w n t1 t2 rs
-          (HW : wptp safe m w n (t1 ++ t2) rs) :
-      exists rs1 rs2, rs1 ++ rs2 = rs /\ wptp safe m w n t1 rs1 /\ wptp safe m w n t2 rs2.
-    Proof.
-      revert rs HW; induction t1; intros; inversion HW; simpl in *; subst; clear HW.
-      - exists (@nil res) (@nil res); now auto using wptp.
-      - exists (@nil res); simpl; now eauto using wptp.
-      - apply IHt1 in WPTP; destruct WPTP as [rs1 [rs2 [EQrs [WP1 WP2] ] ] ]; clear IHt1.
-        exists (r :: rs1) rs2; simpl; subst; now auto using wptp.
-    Qed.
-
-    Lemma comp_list_app rs1 rs2 :
-      comp_list (rs1 ++ rs2) == comp_list rs1 · comp_list rs2.
+    Lemma wptp_app_tp safe m w n t1 t2 rs φs
+          (HW : wptp safe m w n (t1 ++ t2) rs φs) :
+      exists rs1 rs2 φs1 φs2, rs1 ++ rs2 = rs /\ φs1 ++ φs2 = φs /\ wptp safe m w n t1 rs1 φs1 /\ wptp safe m w n t2 rs2 φs2.
     Proof.
-      induction rs1; simpl comp_list; [now rewrite pcm_op_unit by apply _ |].
-      now rewrite IHrs1, assoc.
+      revert rs φs HW; induction t1; intros; inversion HW; simpl in *; subst; clear HW.
+      - do 4 eexists. split; [|split; [|split; now econstructor] ]; reflexivity.
+      - do 4 eexists. split; [|split; [|split; now eauto using wptp] ]; reflexivity.
+      - apply IHt1 in WPTP; destruct WPTP as [rs1 [rs2 [φs1 [φs2 [EQrs [EQφs [WP1 WP2] ] ] ] ] ] ]; clear IHt1.
+        exists (r :: rs1) rs2 (φ :: φs1) φs2; simpl; subst; now auto using wptp.
     Qed.
 
     (* Closure under future worlds and smaller steps *)
-    Lemma wptp_closure safe m (w1 w2 : Wld) n1 n2 tp rs
+    Lemma wptp_closure safe m (w1 w2 : Wld) n1 n2 tp rs φs
           (HSW : w1 ⊑ w2) (HLe : n2 <= n1)
-          (HW : wptp safe m w1 n1 tp rs) :
-      wptp safe m w2 n2 tp rs.
+          (HW : wptp safe m w1 n1 tp rs φs) :
+      wptp safe m w2 n2 tp rs φs.
     Proof.
       induction HW; constructor; [| assumption].
       eapply uni_pred; [eassumption | reflexivity |].
@@ -295,99 +290,88 @@ 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
-          (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) w @ n + S k) :
-      exists w' r',
-        w ⊑ w' /\ φ (exist _ e' HV) w' (S k) r' /\ wsat σ' m (Some r') w' @ S k.
+    Lemma preserve_wptp safe m n k tp tp' σ σ' w rs φs
+          (HSN  : stepn n (tp, σ) (tp', σ'))
+          (HWTP : wptp safe m w (n + S k) tp rs φs)
+          (HE   : wsat σ m (comp_list rs) w @ n + S k) :
+      exists w' rs' φs',
+        w ⊑ w' /\ wptp safe m w' (S k) tp' rs' (φs ++ φs') /\ wsat σ' m (comp_list rs') w' @ S k.
     Proof.
-      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' [HSW [Hφ HE'] ] ] ].
-        rewrite mask_emp_union in HE'; destruct (Some r' · comp_list rs) as [r'' |] eqn: EQr.
-        - 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'. reflexivity.
+      revert tp σ w rs  φs HSN HWTP HE. induction n; intros; inversion HSN; subst; clear HSN.
+      (* no step is taken *)
+      { exists w rs (@nil vPred). split; [reflexivity|]. split.
+        - rewrite List.app_nil_r. assumption.
+        - assumption.
       }
-      rename n0 into n; specialize (HInd n (le_n _)); inversion HS; subst; clear HS.
+      inversion HS; subst; clear HS.
       (* atomic step *)
-      { destruct t1 as [| ee t1]; inversion H0; subst; clear H0.
-        (* 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' [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) (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' [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].
-            * apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
+      { inversion H0; subst; clear H0.
+        apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [φs1 [φs2 [EQrs [EQφs [HWTP1 HWTP2] ] ] ] ] ] ].
+        inversion HWTP2; subst; clear HWTP2; rewrite ->unfold_wp in WPE.
+        edestruct (WPE w (n + S k) (comp_list (rs1 ++ rs0))) as [_ [HS _] ];
+          [reflexivity | now apply le_n | now 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 r)), <- assoc. reflexivity.       
+        + edestruct HS as [w' [r' [HSW [WPE' HE'] ] ] ];
+          [reflexivity | eassumption | clear WPE HS].
+          setoid_rewrite HSW. eapply IHn; clear IHn.
+          * eassumption.
+          * apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
             constructor; [eassumption | eapply wptp_closure, WPTP; [assumption | now auto with arith] ].
-          * eapply wsat_equiv, HE'; try reflexivity; [symmetry; 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 (comp_list rs1)), <- assoc.
+          * eapply wsat_equiv, HE'; [now erewrite mask_emp_union| |reflexivity].
+            rewrite !comp_list_app; simpl comp_list; unfold equiv.
+            rewrite ->2!assoc, (comm (Some r')). reflexivity.
       }
       (* fork *)
-      destruct t1 as [| ee t1]; inversion H; subst; clear H.
-      (* 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 [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].
-        + eapply wsat_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
-          rewrite (comm (Some rfk)), <- assoc; apply pcm_op_equiv; [reflexivity |].
-          rewrite comp_list_app; simpl comp_list; rewrite comm.
-          now erewrite (comm _ 1), pcm_op_unit by apply _.
-      (* 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) (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 [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] |].
-            constructor; [eassumption | apply wptp_app; [| now eauto using wptp] ].
-            eapply wptp_closure, WPTP; [assumption | now auto with arith].
-          * eapply wsat_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
-            rewrite (assoc _ (Some r)), (comm _ (Some r)), <- assoc.
-            apply pcm_op_equiv; [reflexivity |].
-            rewrite (comm (Some rfk)), <- assoc, comp_list_app; simpl comp_list.
-            rewrite assoc, (comm _ (Some rret)), <- assoc.
-            apply pcm_op_equiv; [reflexivity |].
-            rewrite (comm (Some rfk)), !comp_list_app; simpl comp_list.
-            rewrite assoc; apply pcm_op_equiv; [reflexivity |].
-            now erewrite comm, pcm_op_unit by apply _.
-    Qed.
-
-    Lemma unit_min r : pcm_unit _ ⊑ r.
+      inversion H; subst; clear H.
+      apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [φs1 [φs2 [EQrs [EQφs [HWTP1 HWTP2] ] ] ] ] ] ].
+      inversion HWTP2; subst; clear HWTP2; rewrite ->unfold_wp in WPE.
+      edestruct (WPE w (n + S k) (comp_list (rs1 ++ rs0))) as [_ [_ [HF _] ] ];
+        [reflexivity | now apply le_n | now 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 r)), <- assoc. reflexivity.
+      + specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [HSW [WPE' [WPS HE'] ] ] ] ] ]; clear WPE.
+        setoid_rewrite HSW. edestruct IHn as [w'' [rs'' [φs'' [HSW'' [HSWTP'' HSE''] ] ] ] ]; first eassumption; first 2 last.
+        * exists w'' rs'' ([umconst ⊤] ++ φs''). split; [eassumption|].
+          rewrite List.app_assoc. split; eassumption.
+        * rewrite -List.app_assoc. apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
+          constructor; [eassumption|].
+          apply wptp_app; [eapply wptp_closure, WPTP; [assumption | now auto with arith] |].
+          constructor; [|now constructor]. eassumption.
+        * eapply wsat_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
+          rewrite comp_list_app. simpl comp_list. rewrite !comp_list_app. simpl comp_list.
+          rewrite (comm _ 1). erewrite pcm_op_unit by apply _. unfold equiv.
+          rewrite (comm _ (Some rfk)). rewrite ->!assoc. apply pcm_op_equiv;[|reflexivity]. unfold equiv.
+          rewrite <-assoc, (comm (Some rret)), comm. reflexivity.
+    Qed.
+
+
+    Lemma adequate_tp safe m n k e e' tp tp' σ σ' φ w r rs φs
+          (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 φs)
+          (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.
-      exists r; now erewrite comm, pcm_op_unit by apply _.
+      edestruct preserve_wptp as [w' [rs' [φs' [HSW' [HSWTP' HSWS'] ] ] ] ]; first eassumption.
+      - econstructor; eassumption.
+      - assumption.
+      - inversion HSWTP'; subst; clear HSWTP'.
+        rewrite ->unfold_wp in WPE.
+        edestruct (WPE w' k) as [HVal _];
+          [reflexivity | unfold lt; reflexivity | now apply mask_emp_disjoint | rewrite mask_emp_union; eassumption|].
+        fold comp_list in HVal.
+        specialize (HVal HV); destruct HVal as [w'' [r'' [HSW'' [Hφ'' HE''] ] ] ].
+        destruct (Some r'' · comp_list rs0) as [r''' |] eqn: EQr.
+        + exists w'' r'''. split; [etransitivity; eassumption|].
+          split; [|rewrite <-mask_emp_union; assumption].
+          eapply uni_pred, Hφ''; [reflexivity|].
+          rewrite ord_res_optRes. exists (comp_list rs0). rewrite ->comm, EQr. reflexivity.
+        + exfalso. eapply wsat_not_empty, HE''. reflexivity.
     Qed.
 
     (** This is a (relatively) generic adequacy statement for all postconditions; one can
@@ -408,7 +392,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       - simpl comp_list; now erewrite comm, pcm_op_unit by apply _.
     Qed.
 
-    Program Definition cons_pred (φ : value -=> Prop): value -n> Props :=
+    Program Definition cons_pred (φ : value -=> Prop): vPred :=
       n[(fun v => pcmconst (mkUPred (fun n r => φ v) _))].
     Next Obligation.
       firstorder.
@@ -423,14 +407,15 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
     Qed.
 
     (* Adequacy as stated in the paper: for observations of the return value *)
-    Theorem adequacy_obs safe m e (φ : value -=> Prop) n e' tp σ σ'
+    Theorem adequacy_obs safe m e (φ : value -=> Prop) e' tp σ σ'
             (HT  : valid (ht safe m (ownS σ) e (cons_pred φ)))
-            (HSN : stepn n ([e], σ) (e' :: tp, σ'))
+            (HSN : steps ([e], σ) (e' :: tp, σ'))
             (HV : is_value e') :
         φ (exist _ e' HV).
     Proof.
-      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 _.
+      destruct (steps_stepn _ _ HSN) as [n HSN']. clear HSN.
+      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 _.
       - 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].
@@ -450,10 +435,10 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
 
     Existing Instance LP_isval.
 
-    Implicit Types (P Q R : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (φ : value -n> Props) (r : res).
+    Implicit Types (P Q R : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (φ : vPred) (r : res).
 
     (** Ret **)
-    Program Definition eqV v : value -n> Props :=
+    Program Definition eqV v : vPred :=
       n[(fun v' : value => v === v')].
     Next Obligation.
       intros v1 v2 EQv w n r; simpl in *; split; congruence.
@@ -507,17 +492,17 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       ht safe m P e φ ∧ all (plugV safe m φ φ' K) ⊑ ht safe m P (K [[ e ]]) φ'.
     Proof.
       intros wz nz rz [He HK] w HSw n r HLe _ HP.
-      specialize (He _ HSw _ _ HLe (unit_min _) HP).
-      rewrite HSw, <- HLe in HK; clear wz nz HSw HLe HP.
+      specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
+      rewrite ->HSw, <- HLe in HK; clear wz nz HSw HLe HP.
       revert e w r He HK; induction n using wf_nat_ind; intros; rename H into IH.
-      rewrite unfold_wp in He; rewrite unfold_wp.
+      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' [HSw' [Hφ HE] ] ] ].
         (* Fold the goal back into a wp *)
         setoid_rewrite HSw'.
         assert (HT : wp safe m (K [[ e ]]) φ' w'' (S k) r');
-          [| rewrite unfold_wp in HT; eapply HT; [reflexivity | unfold lt; reflexivity | eassumption | eassumption] ].
+          [| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | unfold lt; reflexivity | eassumption | eassumption] ].
         clear HE; specialize (HK (exist _ e HVal)).
         do 30 red in HK; unfold proj1_sig in HK.
         apply HK; [etransitivity; eassumption | apply HLt | apply unit_min | assumption].
@@ -561,26 +546,26 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
     Qed.
     Next Obligation.
       intros v1 v2 EQv; unfold vs.
-      rewrite EQv; reflexivity.
+      rewrite ->EQv; reflexivity.
     Qed.
 
     Lemma htCons P P' φ φ' safe m e :
       vs m m P P' ∧ ht safe m P' e φ' ∧ all (vsLift m m φ' φ) ⊑ ht safe m P e φ.
     Proof.
       intros wz nz rz [ [HP He] Hφ] w HSw n r HLe _ Hp.
-      specialize (HP _ HSw _ _ HLe (unit_min _) Hp); rewrite unfold_wp.
+      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' [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').
+      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');
-        [| rewrite unfold_wp in HT; eapply HT; [reflexivity | apply le_n | eassumption | eassumption] ].
-      unfold lt in HLt; rewrite HSw, HSw', <- HLt in Hφ; clear - He Hφ.
+        [| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | apply le_n | eassumption | eassumption] ].
+      unfold lt in HLt; rewrite ->HSw, HSw', <- HLt in Hφ; clear - He Hφ.
       (* Second phase of the proof: got rid of the preconditions,
          now induction takes care of the evaluation. *)
       rename r' into r; rename w'' into w.
       revert w r e He Hφ; generalize (S k) as n; clear k; induction n using wf_nat_ind.
-      rename H into IH; intros; rewrite unfold_wp; rewrite unfold_wp in He.
+      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' [HSw' [Hφ' HE] ] ] ].
@@ -592,11 +577,11 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         try eassumption; clear HS.
         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φ.
+        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
       - 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φ.
+        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
       - assumption.
     Qed.
 
@@ -606,7 +591,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       vs m m' P P' ∧ ht safe m' P' e φ' ∧ all (vsLift m' m φ' φ) ⊑ ht safe m P e φ.
     Proof.
       intros wz nz rz [ [HP He] Hφ] w HSw n r HLe _ Hp.
-      specialize (HP _ HSw _ _ HLe (unit_min _) Hp); rewrite unfold_wp.
+      specialize (HP _ HSw _ _ HLe (unit_min _ _) Hp); rewrite unfold_wp.
       split; [intros HV; contradiction (atomic_not_value e) |].
       edestruct HP as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [|]; clear HP.
       { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
@@ -614,21 +599,21 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       }
       split; [| split; [intros; subst; contradiction (fork_not_atomic K e') |] ].
       - intros; rewrite <- HLe, HSw in He, Hφ; clear wz nz HSw HLe Hp.
-        clear HE; rewrite HSw0 in He; specialize (He w'' HSw' _ r' HLt (unit_min _) Hp').
-        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 |].
+        clear HE; rewrite ->HSw0 in He; specialize (He w'' HSw' _ r' HLt (unit_min _ _) Hp').
+        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'' [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.
-        rewrite fill_empty in *; rename ei into e.
+        rewrite ->fill_empty in *; rename ei into e.
         setoid_rewrite HSw'; setoid_rewrite HSw.
         assert (HVal := atomic_step _ _ _ _ HAt HStep).
-        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 |].
+        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 [HSw [Hφ' HE] ] ] ].
         eapply Hφ in Hφ'; [| assumption | apply Le.le_n_Sn | apply unit_min].
         clear Hφ; edestruct Hφ' as [w'' [r' [HSw' [Hφ HE'] ] ] ];
@@ -638,18 +623,18 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         }
         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 |] ] ].
+        clear - Hφ; rewrite ->unfold_wp; intros w; intros; split; [intros HVal' | split; intros; [intros; exfalso|split; [intros |] ] ].
         + do 2 eexists; split; [reflexivity | split; [| eassumption] ].
-          unfold lt in HLt; rewrite HLt, <- HSw.
+          unfold lt in HLt; rewrite ->HLt, <- HSw.
           eapply φ, Hφ; [| apply le_n]; simpl; reflexivity.
         + eapply values_stuck; [.. | repeat eexists]; eassumption.
         + clear - HDec HVal; subst; assert (HT := fill_value _ _ HVal); subst.
-          rewrite fill_empty in HVal; now apply fork_not_value in HVal.
+          rewrite ->fill_empty in HVal; now apply fork_not_value in HVal.
         + intros; left; assumption.
       - clear Hφ; intros; rewrite <- HLe, HSw in He; clear HLe HSw.
-        specialize (He w'' (transitivity HSw0 HSw') _ r' HLt (unit_min _) Hp').
-        rewrite unfold_wp in He; edestruct He as [_ [_ [_ HS'] ] ];
-          [reflexivity | apply le_n | rewrite HSub; eassumption | eassumption |].
+        specialize (He w'' (transitivity HSw0 HSw') _ r' HLt (unit_min _ _) Hp').
+        rewrite ->unfold_wp in He; edestruct He as [_ [_ [_ HS'] ] ];
+          [reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
         auto.
     Qed.
 
@@ -660,7 +645,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       wp safe m1 e φ ⊑ wp safe (m1 ∪ m2) e φ.
     Proof.
       intros w n; revert w e φ; induction n using wf_nat_ind; rename H into HInd; intros w e φ r HW.
-      rewrite unfold_wp; rewrite unfold_wp in HW; intros w'; intros.
+      rewrite unfold_wp; rewrite ->unfold_wp in HW; intros w'; intros.
       edestruct HW with (mf := mf ∪ m2) as [HV [HS [HF HS'] ] ]; try eassumption;
       [| eapply wsat_equiv, HE; try reflexivity; [] |].
       { intros j [ [Hmf | Hm'] Hm]; [apply (HD0 j) | apply (HD j) ]; tauto.
@@ -688,33 +673,33 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       ht safe m P e φ ⊑ ht safe (m ∪ m') (P * R) e (lift_bin sc φ (umconst R)).
     Proof.
       intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
-      specialize (He _ HSw _ _ HLe (unit_min _) HP).
+      specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
       clear P w n rz HSw HLe HP; rename w' into w; rename n' into n.
       apply wp_mask_weaken; [assumption |]; revert e w r1 r EQr HLR He.
       induction n using wf_nat_ind; intros; rename H into IH.
-      rewrite unfold_wp; rewrite unfold_wp in He; intros w'; intros.
+      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' [HSw' [Hφ HE] ] ] ].
-        rewrite assoc in HE; destruct (Some r1' · Some r2) as [r' |] eqn: EQr';
+        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 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.
+        exists r1' r2; split; [now rewrite ->EQr' | split; [assumption |] ].
+        unfold lt in HLt; rewrite ->HLt, <- HSw', <- HSw; apply HLR.
       - 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';
+        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 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.
+        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
       - 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;
+        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 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.
+        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
       - auto.
     Qed.
 
@@ -724,17 +709,17 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
       ht safe m P e φ ⊑ ht safe (m ∪ m') (P * ▹ R) e (lift_bin sc φ (umconst R)).
     Proof.
       intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
-      specialize (He _ HSw _ _ HLe (unit_min _) HP).
-      clear rz n HLe; apply wp_mask_weaken; [assumption |]; rewrite unfold_wp.
+      specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
+      clear rz n HLe; apply wp_mask_weaken; [assumption |]; rewrite ->unfold_wp.
       clear w HSw; rename n' into n; rename w' into w; intros w'; intros.
       split; [intros; exfalso | split; intros; [| split; intros; [exfalso| ] ] ].
       - contradiction (atomic_not_value e).
       - destruct k as [| k];
         [exists w' r; split; [reflexivity | split; [apply wpO | exact I] ] |].
-        rewrite unfold_wp in He; rewrite <- EQr, <- assoc in HE.
+        rewrite ->unfold_wp in He; rewrite <- EQr, <- assoc in HE.
         edestruct He as [_ [HeS _] ]; try eassumption; [].
         edestruct HeS as [w'' [r1' [HSw' [He' HE'] ] ] ]; try eassumption; [].
-        clear HE He HeS; rewrite assoc in HE'.
+        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 _] ].
@@ -742,26 +727,26 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
         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.
-        rewrite fill_empty in *.
+        rewrite ->fill_empty in *.
         unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; simpl in HLR.
         assert (HVal := atomic_step _ _ _ _ HAt HStep).
-        clear - He' HVal EQr' HLR; rename w'' into w; rewrite unfold_wp; intros w'; intros.
+        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; [].
+        + rewrite ->unfold_wp in He'; rewrite <- EQr', <- assoc in HE; edestruct He' as [HVal _]; try eassumption; [].
           specialize (HVal HV); destruct HVal as [w'' [r1'' [HSw' [Hφ HE'] ] ] ].
-          rewrite assoc in HE'; destruct (Some r1'' · Some r2) as [r'' |] eqn: EQr'';
+          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 2 eexists; split; [eassumption | split; [| eassumption] ].
-          exists r1'' r2; split; [now rewrite EQr'' | split; [assumption |] ].
+          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.
         + subst; clear -HVal.
-          assert (HT := fill_value _ _ HVal); subst K; rewrite fill_empty in HVal.
+          assert (HT := fill_value _ _ HVal); subst K; rewrite ->fill_empty in HVal.
           contradiction (fork_not_value e').
         + auto.
       - subst; eapply fork_not_atomic; eassumption.
-      - rewrite <- EQr, <- assoc in HE; rewrite unfold_wp in He.
+      - rewrite <- EQr, <- assoc in HE; rewrite ->unfold_wp in He.
         specialize (He w' k (Some r2 · rf) mf σ HSw HLt HD0 HE); clear HE.
         destruct He as [_ [_ [_ HS'] ] ]; auto.
     Qed.
@@ -772,29 +757,29 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
     Proof.
       intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
       destruct n' as [| n']; [apply wpO |].
-      simpl in HP; specialize (He _ HSw _ _ (Le.le_Sn_le _ _ HLe) (unit_min _) HP).
-      clear rz n HLe; rewrite unfold_wp.
+      simpl in HP; specialize (He _ HSw _ _ (Le.le_Sn_le _ _ HLe) (unit_min _ _) HP).
+      clear rz n HLe; rewrite ->unfold_wp.
       clear w HSw HP; rename n' into n; rename w' into w; intros w'; intros.
       split; [intros; contradiction (fork_not_value e) | split; intros; [exfalso | split; intros ] ].
-      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite fill_empty in HDec; subst.
+      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite ->fill_empty in HDec; subst.
         eapply fork_stuck with (K := ε); [| repeat eexists; eassumption ]; reflexivity.
-      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite fill_empty in HDec.
+      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite ->fill_empty in HDec.
         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 3 eexists; split; [reflexivity | split; [| split; eassumption] ].
-        rewrite fill_empty; rewrite unfold_wp; rewrite <- (le_S_n _ _ HLt), HSw in HLR.
+        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 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.
         + eapply values_stuck; [exact fork_ret_is_value | eassumption | repeat eexists; eassumption].
-        + assert (HV := fork_ret_is_value); rewrite HDec in HV; clear HDec.
-          assert (HT := fill_value _ _ HV);subst K; rewrite fill_empty in HV.
+        + assert (HV := fork_ret_is_value); rewrite ->HDec in HV; clear HDec.
+          assert (HT := fill_value _ _ HV);subst K; rewrite ->fill_empty in HV.
           eapply fork_not_value; eassumption.
         + left; apply fork_ret_is_value.
-      - right; right; exists e empty_ctx; rewrite fill_empty; reflexivity.
+      - right; right; exists e empty_ctx; rewrite ->fill_empty; reflexivity.
     Qed.
 
   End HoareTripleProperties.
@@ -807,12 +792,12 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
 
     Existing Instance LP_isval.
 
-    Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (φ : value -n> Props) (r : res).
+    Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (φ : vPred) (r : res).
 
     Lemma vsFalse m1 m2 :
       valid (vs m1 m2 ⊥ ⊥).
     Proof.
-      rewrite valid_iff, box_top.
+      rewrite ->valid_iff, box_top.
       unfold vs; apply box_intro.
       rewrite <- and_impl, and_projR.
       apply bot_false.
diff --git a/lang.v b/lang.v
index 5a33d268a09f490b5bf53c0865814e650c4ab2d9..f8d03d17002bdc2e295b8e4aecefd39da7d4515b 100644
--- a/lang.v
+++ b/lang.v
@@ -159,4 +159,31 @@ Module Lang (C : CORE_LANG).
     - symmetry in EQK; now apply fill_noinv in EQK.
   Qed.
 
+  (* Reflexive, transitive closure of the step relation *)
+  Inductive steps : cfg -> cfg -> Prop :=
+  | steps_refl ρ : steps ρ ρ
+  | stepn_trans ρ1 ρ2 ρ3 : step ρ1 ρ2 -> steps ρ2 ρ3 -> steps ρ1 ρ3.
+                     
+  
+  Inductive stepn : nat -> cfg -> cfg -> Prop :=
+  | stepn_O ρ : stepn O ρ ρ
+  | stepn_S ρ1 ρ2 ρ3 n
+            (HS  : step ρ1 ρ2)
+            (HSN : stepn n ρ2 ρ3) :
+      stepn (S n) ρ1 ρ3.
+
+  Lemma steps_stepn ρ1 ρ2:
+    steps ρ1 ρ2 -> exists n, stepn n ρ1 ρ2.
+  Proof.
+    induction 1.
+    - eexists. eauto using stepn.
+    - destruct IHsteps as [n IH]. eexists. eauto using stepn.
+  Qed.
+
+  Lemma stepn_steps n ρ1 ρ2:
+    stepn n ρ1 ρ2 -> steps ρ1 ρ2.
+  Proof.
+    induction 1; now eauto using steps.
+  Qed.
+
 End Lang.
diff --git a/lib/ModuRes/PCM.v b/lib/ModuRes/PCM.v
index fd8e93bb4e9f9ad2f1f4e57bdad47f233dff7634..5d5a619f5129ccdcdc0769875612dd067895ee76 100644
--- a/lib/ModuRes/PCM.v
+++ b/lib/ModuRes/PCM.v
@@ -150,6 +150,11 @@ Section Order.
        erewrite pcm_op_zero in EQ by apply _; contradiction.
   Qed.
 
+  Lemma unit_min r : pcm_unit _ ⊑ r.
+  Proof.
+    exists r; now erewrite comm, pcm_op_unit by apply _.
+  Qed.
+
 End Order.
 
 Section Exclusive.