diff --git a/core_lang.v b/core_lang.v
index f151241f84b0c81bf01cd77e37dbb054a817cfd1..b45735a70342b6582dd8ca7ec365de56815f6912 100644
--- a/core_lang.v
+++ b/core_lang.v
@@ -7,7 +7,7 @@ Module Type CORE_LANG.
   (******************************************************************)
 
   (** Expressions and values **)
-  Parameter expr : Type.
+  Parameter expr : Type.	(* PDS: setoid. *)
 
   Parameter is_value : expr -> Prop.
   Definition value : Type := {e: expr | is_value e}.
@@ -24,7 +24,7 @@ Module Type CORE_LANG.
                      fork e1 = fork e2 -> e1 = e2.
 
   (** Evaluation contexts **)
-  Parameter ectx : Type.
+  Parameter ectx : Type.	(* PDS: setoid. *)
   Parameter empty_ctx : ectx.
   Parameter comp_ctx : ectx -> ectx -> ectx.
   Parameter fill : ectx -> expr -> expr.
@@ -48,7 +48,7 @@ Module Type CORE_LANG.
                        K = ε.
 
   (** Shared machine state (e.g., the heap) **)
-  Parameter state : Type.
+  Parameter state : Type.	(* PDS: setoid. *)
 
   (** Primitive (single thread) machine configurations **)
   Definition prim_cfg : Type := (expr * state)%type.
diff --git a/iris_core.v b/iris_core.v
index 0864d1233f788800b920a757a007b3cf87e2fc46..3b895140574765dfe35d486111f73f6c744ddd93 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -5,12 +5,13 @@ Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finma
 Set Bullet Behavior "Strict Subproofs".
 
 (* Because Coq has a restriction of how to apply functors, we have to hack a bit here.
+   PDS: "a bit"?! Hahaha.
    The hack that involves least work, is to duplicate the definition of our final
    resource type, as a module type (which is how we can use it, circumventing the
    Coq restrictions) and as a module (to show the type can be instantiated). *)
 Module Type IRIS_RES (RL : RA_T) (C : CORE_LANG) <: RA_T.
   Instance state_type : Setoid C.state := discreteType.
-  
+ 
   Definition res := (ra_res_ex C.state * RL.res)%type.
   Instance res_type : Setoid res := _.
   Instance res_op   : RA_op res := _.
@@ -70,11 +71,31 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
   Instance Props_BI : ComplBI Props | 0 := _.
   Instance Props_Later : Later Props | 0 := _.
-  
+ 
   (** And now we're ready to build the IRIS-specific connectives! *)
 
   Implicit Types (P Q : Props) (w : Wld) (n i k : nat) (m : mask) (r u v : res) (σ : state).
 
+  Section Resources.
+
+    (* PDS: These should probably be split into RA-level and resource-level lemmas. *)
+
+    Lemma ex_frame {σ f} : ↓((ex_own state σ,1:RL.res)·f) -> fst f == 1.
+    Proof.
+      move: f=>[fx fg]; rewrite/ra_op/res_op/ra_op_prod/fst.
+      move=>[Hx _]; move: Hx {fg}; rewrite/ra_op/ra_op_ex.
+      by case: fx.
+    Qed.
+  
+    Lemma ex_fpu {σ σ' u} : ↓((ex_own state σ, 1:RL.res) · u) -> ↓((ex_own state σ', 1:RL.res) · u).
+    Proof.
+      move=> Hv; move: (ex_frame Hv)=> Hxu; move: Hxu Hv.
+      move: u=>[ux ug]; rewrite/fst; move=>->.
+      by rewrite /ra_op/res_op/ra_op_prod ra_op_unit.
+    Qed.
+
+  End Resources.
+
   Section Necessitation.
     (** Note: this could be moved to BI, since it's possible to define
         for any UPred over a RA. **)
@@ -99,6 +120,12 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       apply EQp; assumption.
     Qed.
 
+    Global Program Instance box_dist n : Proper (dist n ==> dist n) box.
+    Next Obligation.
+      move=> P P' HEq w k r HLt.
+      exact: (HEq w).
+    Qed.
+
   End Necessitation.
 
   Notation "â–¡ P" := (box P) (at level 30, right associativity) : iris_scope.
@@ -138,6 +165,21 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
     - intros [r1 [r2 [_ [HP _] ] ] ]. assumption.
   Qed.
 
+  Section BoxAll.
+    Context {T} `{cT : cmetric T}.
+    Context (φ : T -n> Props).
+  
+    Program Definition box_all_lhs : Props := ∀t, □φ t.
+    Next Obligation.
+      move=> t t' HEq.
+      apply: box_dist.
+      exact: (met_morph_nonexp _ _ φ).
+    Qed.
+  
+    Lemma box_all : □all φ == box_all_lhs.
+    Proof. done. Qed.
+  End BoxAll.
+
   (** "Internal" equality **)
   Section IntEq.
     Context {T} `{mT : metric T}.
@@ -171,10 +213,10 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
   Notation "t1 '===' t2" := (intEq t1 t2) (at level 70) : iris_scope.
 
   Section Timeless.
-  
+ 
     Definition timelessP P w n :=
       forall w' k r (HSw : w ⊑ w') (HLt : k < n) (Hp : P w' k r), P w' (S k) r.
-  
+ 
     Program Definition timeless P : Props :=
       m[(fun w => mkUPred (fun n r => timelessP P w n) _)].
     Next Obligation.
@@ -193,7 +235,7 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       intros w1 w2 HSw n; simpl; intros _ HT w' m r HSw' HLt Hp.
       eapply HT, Hp; [etransitivity |]; eassumption.
     Qed.
-  
+ 
   End Timeless.
 
   Section IntEqTimeless.
@@ -232,7 +274,7 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
     Lemma ownR_timeless {u} :
       valid(timeless(ownR u)).
     Proof. intros w n _ w' k r _ _; now auto. Qed.
-  
+ 
     Lemma ownR_sc u v:
       ownR (u · v) == ownR u * ownR v.
     Proof.
@@ -259,7 +301,15 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
     Lemma ownS_timeless {σ} : valid(timeless(ownS σ)).
     Proof. exact ownR_timeless. Qed.
-  
+
+    Lemma ownS_state {σ w n r} (Hv : ↓r) :
+      (ownS σ) w n r -> fst r == ex_own state σ.
+    Proof.
+      move: Hv; move: r => [rx _] [Hv _] [ [x _] /= [Hr _] ].
+      move: Hv; rewrite -Hr {Hr}.
+      by case: x.
+    Qed.
+
     (** Proper ghost state: ownership of logical **)
     Program Definition ownL : RL.res -n> Props :=
       n[(fun r : RL.res => ownR (1, r))].
@@ -270,7 +320,7 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
     Lemma ownL_timeless {r : RL.res} : valid(timeless(ownL r)).
     Proof. exact ownR_timeless. Qed.
-  
+ 
     (** Ghost state ownership **)
     Lemma ownL_sc (r s : RL.res) :
       ownL (r · s) == ownL r * ownL s.
diff --git a/iris_ht_rules.v b/iris_ht_rules.v
index 203e9d70c28962e72e3c60e4bdbd0bb38d93a131..7bf2468e86c2864a5d35f3c815e5ce0a1b8009f1 100644
--- a/iris_ht_rules.v
+++ b/iris_ht_rules.v
@@ -56,8 +56,6 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         rewrite EQv; reflexivity.
     Qed.
 
-    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
     Lemma htBind P Q R K e safe m :
       ht safe m P e Q ∧ all (plugV safe m Q R K) ⊑ ht safe m P (K [[ e ]]) R.
     Proof.
diff --git a/iris_meta.v b/iris_meta.v
index 5f65742ad9913c595981c5b0d2ce1caa1807930e..790aad26a9da2dc8ecf36e69276d09dcfbf87772 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -77,7 +77,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
           [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 r), <- assoc. reflexivity.       
+          rewrite ->assoc, (comm r), <- assoc. reflexivity.
         + edestruct HS as [w' [r' [HSW [WPE' HE'] ] ] ];
           [reflexivity | eassumption | clear WPE HS].
           setoid_rewrite HSW. eapply IHn; clear IHn.
@@ -156,7 +156,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       - intros _. simpl. assert(H_xy': x == y) by assumption. rewrite H_xy'. tauto.
     Qed.
 
-      
+
     (* Adequacy as stated in the paper: for observations of the return value, after termination *)
     Theorem adequacy_obs safe m e (Q : value -=> Prop) e' tp' σ σ'
             (HT  : valid (ht safe m (ownS σ) e (lift_vPred Q)))
@@ -197,11 +197,8 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
   End Adequacy.
 
-  Set Bullet Behavior "None".	(* PDS: Ridiculous. *)
   Section RobustSafety.
 
-    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
     Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : res) (w : Wld) (σ : state).
 
     Program Definition restrictV (Q : expr -n> Props) : vPred :=
@@ -211,7 +208,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       case: n=>[_ Hk | n]; first by exfalso; omega.
       by move=> /= ->.
     Qed.
-  
+
     (*
      * Primitive reductions are either pure (do not change the state)
      * or atomic (step to a value).
@@ -229,17 +226,18 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
     (* Compatibility for those expressions wp cares about. *)
     Hypothesis forkE : forall e, E (fork e) == E e.
     Hypothesis fillE : forall K e, E (K [[e]]) == E e * E (K [[fork_ret]]).
-    
+
     (* One can prove forkE, fillE as valid internal equalities. *)
     (* RJ: We don't have rules for internal equality of propositions, don't we? Maybe we should have an axiom,
        saying they are equal iff they are equivalent. *)
+    (* PDS: Would you like to flush out §5.1 of the appendix? *)
     Remark valid_intEq {P P' : Props} (H : valid(P === P')) : P == P'.
     Proof. move=> w n r; exact: H. Qed.
 
     (* View shifts or atomic triples for every primitive reduction. *)
     Variable wâ‚€ : Wld.
     Definition valid₀ P := forall w n r (HSw₀ : w₀ ⊑ w), P w n r.
-    
+
     Hypothesis pureE : forall {e σ e'},
       prim_step (e,σ) (e',σ) ->
       validâ‚€ (vs mask_full mask_full (E e) (E e')).
@@ -252,7 +250,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
     Proof.
       move=> wz nz rz HSwâ‚€ w HSw n r HLe _ He.
       have {HSw₀ HSw} HSw₀ : w₀ ⊑ w by transitivity wz.
-      
+
       (* For e = K[fork e'] we'll have to prove wp(e', ⊤), so the IH takes a post. *)
       pose post Q := forall (v : value) w n r, (E (`v)) w n r -> (Q v) w n r.
       set Q := restrictV E; have HQ: post Q by done.
@@ -262,22 +260,22 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       split; [| split; [| split; [| done] ] ]; first 2 last.
 
       (* e forks: fillE, IH (twice), forkE *)
-      - move=> e' K HDec.
+      { move=> e' K HDec.
         have {He} He: (E e) w' k r by propsM He.
-        move: He; rewrite HDec fillE; move=> [re' [rK [Hr [He' HK] ] ] ].   
+        move: He; rewrite HDec fillE; move=> [re' [rK [Hr [He' HK] ] ] ].
         exists w' re' rK; split; first by reflexivity.
         have {IH} IH: forall Q, post Q ->
           forall e r, (E e) w' k r -> wp false mask_full e Q w' k r.
-        + by move=> Q0 HQ0 e0 r0 He0; apply: (IH _ HLt); first by transitivity w.
+        { by move=> Q0 HQ0 e0 r0 He0; apply: (IH _ HLt); first by transitivity w. }
         split; [exact: IH | split]; last first.
-        + by move: HW; rewrite -Hr => HW; wsatM HW.
+        { by move: HW; rewrite -Hr => HW; exact: (wsatM _ HW). }
         have Htop: post (umconst ⊤) by done.
-        by apply: (IH _ Htop e' re'); move: He'; rewrite forkE.
+        by apply: (IH _ Htop e' re'); move: He'; rewrite forkE. }
 
       (* e value: done *)
-      - move=> {IH} HV; exists w' r; split; [by reflexivity | split; [| done] ].
-        by apply: HQ; propsM He.
-      
+      { move=> {IH} HV; exists w' r; split; [by reflexivity | split; [| done] ].
+        by apply: HQ; propsM He. }
+
       (* e steps: fillE, atomic_dec *)
       move=> σ' ei ei' K HDec HStep.
       have {HSw₀} HSw₀ : w₀ ⊑ w' by transitivity w.
@@ -285,15 +283,15 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       move: HW; rewrite -Hr => HW.
       (* bookkeeping common to both cases. *)
       have {Hei} Hei: (E ei) w' (S k) rei by propsM Hei.
-      have HSw': w' ⊑ w' by reflexivity.
-      have HLe: S k <= S k by omega.
+      set HSw' := prefl w'.
+      set HLe := lerefl (S k).
       have H1ei: 1 ⊑ rei by apply: unit_min.
-      have HLt': k < S k by omega.
+      have HLt': k < S k by done.
       move: HW; rewrite {1}mask_full_union -{1}(mask_full_union mask_emp) -assoc => HW.
       case: (atomic_dec ei) => HA; last first.
-      
+
       (* ei pure: pureE, IH, fillE *)
-      - move: (pure_step _ _ _ _ HA HStep) => {HA} Hσ.
+      { move: (pure_step _ _ _ _ HA HStep) => {HA} Hσ.
         rewrite Hσ in HStep HW => {Hσ}.
         move: (pureE _ _ _ HStep) => {HStep} He.
         move: {He} (He w' (S k) r HSwâ‚€) => He.
@@ -303,11 +301,11 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
         move: HW; rewrite assoc=>HW.
         have {HSw₀} HSw₀: w₀ ⊑ w'' by transitivity w'.
         exists w'' (r' · rK); split; [done| split]; last first.
-        + by move: HW; rewrite 2! mask_full_union => HW; wsatM HW.
+        { by move: HW; rewrite 2! mask_full_union => HW; exact: (wsatM _ HW). }
         apply: (IH _ HLt _ _ _ _ HSwâ‚€); last done.
         rewrite fillE; exists r' rK; split; [exact: equivR | split; [by propsM Hei' |] ].
         have {HSw} HSw: w ⊑ w'' by transitivity w'.
-        by propsM HK.
+        by propsM HK. }
 
       (* ei atomic: atomicE, IH, fillE *)
       move: (atomic_step _ _ _ _ HA HStep) => HV.
@@ -323,7 +321,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       (* unroll wp(ei',E)—value case—to get E ei' *)
       move: He'; rewrite {1}unfold_wp => He'.
       move: HW; case Hk': k => [| k'] HW.
-      - by exists w'' r'; split; [done | split; [exact: wpO | done] ].
+      { by exists w'' r'; split; [done | split; [exact: wpO | done] ]. }
       have HSw'': w'' ⊑ w'' by reflexivity.
       have HLt': k' < k by omega.
       move: {He' HSw'' HLt' HD HW} (He' _ _ _ _ _ HSw'' HLt' HD HW) => [Hv _].
@@ -340,15 +338,133 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       have {HSw HSw' HSw''} HSw: w ⊑ w''' by transitivity w''; first by transitivity w'.
       by propsM HK.
     Qed.
-    
+
   End RobustSafety.
-  Set Bullet Behavior "Strict Subproofs".
+
+  Section StatefulLifting.
+
+    Implicit Types (P : Props) (n k : nat) (safe : bool) (m : mask) (e : expr) (r : res) (σ : state) (w : Wld).
+
+    (* A bit too specific to hoist to iris_plog.v without cause. *)
+    Lemma ownS_wsat {σ w n r σ' m u k}
+        (Hr : (ownS σ) w n r)
+        (HW : wsat σ' m u w @ S k)
+        (Hu : r ⊑ u) :
+      σ == σ'.
+    Proof.
+      move: (ra_valid_ord _ _ _ Hu (wsat_valid HW)) => Hv.
+      move/(ownS_state Hv): Hr; move=>{n}; move/wsat_state: HW; move=>{m w k Hv}.
+      move: Hu=>[ [r'x r'g] [Hx Hg] ]; move: Hx Hg.
+      move: u=> [ux ug]; move: r=> [rx rg].
+      rewrite ra_op_prod_fst 3!/fst.
+      move=> Hux _ HD Hrx; move: Hux; move: Hrx->; move=>{r'g ug rg}.
+      case: HD=>->; last by case: r'x.
+      case: r'x=>[σ''||]; [done | | done].
+      by rewrite ra_op_unit; elim.
+    Qed.
+
+    Implicit Types (φ : expr * state -=> Prop).
+    Implicit Types (Q : vPred).
+
+    (* Obligation common to lift_pred and lemma statement. *)
+    Program Instance lift_pred_dist (φ : expr * state -> Props) n : Proper (dist n ==> dist n) φ.
+    Next Obligation.
+      move=> [e'1 σ'1] [e'2 σ'2] HEq w k r HLe.
+      move: HEq HLe; case: n=>[|n] HEq HLt; first by exfalso; exact: lt0.
+      by move: HEq=>/=[-> ->].
+    Qed.
+
+    Program Definition lift_pred φ : expr * state -n> Props :=
+      n[(fun c => pcmconst(mkUPred(fun n r => φ c) _))].
+    Next Obligation. done. Qed.
+
+    Lemma lift_step {m safe e σ φ P Q}
+        (RED : reducible e)
+        (STEP : forall e' σ', prim_step (e,σ) (e',σ') -> φ(e',σ'))
+        (SAFE : if safe then safeExpr e σ else True) :
+      (∀c, let: (e',σ') := c in lift_pred φ (e',σ') → ht safe m (P * ownS σ') e' Q)
+        ⊑ ht safe m (▹P * ownS σ) e Q.
+    Proof.
+      move=> wz nz rz Hfrom w1 HSw1 n r HLe _ HPS.
+      rewrite unfold_wp; move=> w2 k rf mf σi HSw2 HLt _ HW.
+      have Hσ: σ == σi.
+      { clear - HPS HW HSw2.
+        move: HPS => [r1 [r2 [Hr [_ /(propsMW HSw2) HS ] ] ] ] {HSw2}.
+        apply: (ownS_wsat HS HW); move=> {HS HW}.
+        exists (r1 · rf); move: Hr=><-.
+        by rewrite -{1}assoc  [rf · _]comm {1}assoc; reflexivity. }
+      split; [| split; [| split ] ]; first 2 last.
+      { move=> e' K HDec; exfalso; exact: (reducible_not_fork RED HDec). }
+      { by move: SAFE {Hfrom}; rewrite Hσ; case: safe. }
+      { move=> HV; exfalso; exact: reducible_not_value. }
+
+      move=> σ' ei e' K HDec HStep {SAFE}.
+      move: HW HStep; rewrite -Hσ => HW HStep {Hσ}.
+      have HK: K = ε.
+      { move: HDec; rewrite eq_sym_iff -(fill_empty e) => HDec.
+        have HRed1: reducible ei by exists σ (e',σ').
+        by apply: (step_same_ctx _ _ _ _ HDec HRed1 RED). }
+      move: HDec HStep; rewrite HK 2!fill_empty; move=><- HStep {ei K HK RED}.
+
+      (* have φ(e',σ'), so we can apply the triple… *)
+      move/STEP: HStep => He' {STEP}.
+
+      (* … after building P * ownS σ' *)
+      move: HPS HLe HLt; case: n=>[| n'] HPS HLe HLt; first by exfalso; exact: lt0.
+      move: HPS => [rP [rS [Hr [HP [rSg HrS] ] ] ] ]; rewrite/= in HP.
+      pose (rS' := (ex_own state σ', 1:RL.res)).
+      pose (r' := rP · rS').
+      have HPS: (P * ownS σ') w2 k r'.
+      { have {HLt} HLt: k <= n' by omega.
+        move/(propsMW HSw2): HP; move/(propsMN HLt) => HP.
+        have HS': (ownS σ') w2 k rS' by exists 1; rewrite ra_op_unit; split; reflexivity.
+        exists rP rS'; split; [by reflexivity | split; [done | done] ]. }
+      move/(_ (e',σ') _ HSw1 _ rz (lerefl nz) (prefl rz) He'): {He'} Hfrom => He'.
+      have {HLe HLt} HLe: k <= nz by omega.
+      move/(_ _ HSw2 _ r' HLe (unit_min _ _) HPS): He' => He' {HLe HPS}.
+
+      (* wsat σ' r' follows from wsat σ r (by the construction of r'). *)
+      exists w2 r'; split; [by reflexivity | split; [done |] ].
+      have HLe: k <= S k by omega.
+      move/(wsatM HLe): HW; move=>{He' HLe}.
+      case: k=>[| k]; first done; move=>[rs [Hstate HWld] ].
+      exists rs; split; last done.
+      clear - Hr HrS Hstate; move: Hstate=>[Hv _]; move: Hv.
+      rewrite -Hr -HrS /r'/= => {Hr HrS r' rS}.
+      rewrite (* ((P(gσ))f)s *) [rP · _]comm -3!assoc =>/ra_opV2 Hv {rSg}.  (* ((σP)f)s *)
+      rewrite (* ((Pσ')f)s *) [rP · _]comm -2!assoc. (* σ'(P(fs)) *)
+      split; first by exact: (ex_fpu Hv).
+      rewrite/rS' ra_op_prod_fst.
+      move/ex_frame: Hv =>->.
+      exact: ra_op_unit2.
+    Qed.
+    
+    Program Definition lift_post φ : value -n> Props :=
+      n[(fun v => ∃σ', ownS σ' ∧ lift_pred φ (`v, σ'))].
+    Next Obligation.
+      move=> σ σ' HEq w k r HLt.
+      move: HEq HLt; case: n=>[|n] HEq HLt; first by exfalso; omega.
+      by move: HEq=>/=->.
+    Qed.
+    Next Obligation.
+      move=> v v' HEq w k r HLt.
+      move: HEq HLt; case: n=>[|n] HEq HLt; first by exfalso; omega.
+      by move: HEq=>/=->.
+    Qed.
+
+    Lemma lift_atomic_det {m safe e σ φ P Q}
+        (AT : atomic e)
+        (STEP : forall e' σ', prim_step (e,σ) (e',σ') -> φ(e',σ'))
+        (SAFE : if safe then safeExpr e σ else True) :
+      valid(ht safe m (ownS σ) e (lift_post φ)).
+    Abort.
+    
+  End StatefulLifting.
 
   Section Lifting.
 
     Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q R : vPred) (r : res).
 
-
     Program Definition lift_ePred (φ : expr -=> Prop) : expr -n> Props :=
       n[(fun v => pcmconst (mkUPred (fun n r => φ v) _))].
     Next Obligation.
@@ -372,15 +488,13 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
             (RED  : reducible e)
             (STEP : forall σ e2 σ2, prim_step (e, σ) (e2, σ2) -> σ2 = σ /\ φ e2):
       (all (plugExpr safe m φ P Q)) ⊑ ht safe m (▹P) e Q.
-    Proof.
-    Admitted.
+    Abort.
 
     Lemma lift_pure_deterministic_step safe m e e' P Q
           (RED  : reducible e)
           (STEP : forall σ e2 σ2, prim_step (e, σ) (e2, σ2) -> σ2 = σ /\ e2 = e):
       ht safe m P e' Q ⊑ ht safe m (▹P) e Q.
-    Proof.
-    Admitted.
+    Abort.
 
   End Lifting.
 
diff --git a/iris_plog.v b/iris_plog.v
index 3df7d55d8804d273e73a536cb1c1aec6c3202595..3b6d7c4714bbd80584d867b4e621c146807a9803 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -158,13 +158,22 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
         apply HR; [reflexivity | assumption].
     Qed.
 
-    Lemma wsat_valid σ m (r: res) w k :
+    Lemma wsat_valid {σ m r w k} :
       wsat σ m r w (S k) tt -> ↓r.
     Proof.
       intros [rs [HD _] ]. destruct HD as [VAL _].
       eapply ra_op_valid; [now apply _|]. eassumption.
     Qed.
 
+    Lemma wsat_state {σ m u w k} :
+      wsat σ m u w (S k) tt -> fst u == ex_own state σ \/ fst u == 1.
+    Proof.
+      move: u=>[ux ug]; move=>[rs [ [ Hv Heq] _] ] {m w k}; move: Hv Heq.
+      move: (comp_map _)=> [rsx rsg] [Hv _] {rs}; move: Hv.
+      rewrite ra_op_prod_fst 2![fst _]/=.
+      by case: ux; case: rsx; auto.
+    Qed.
+
   End WorldSatisfaction.
 
   Notation " P @ k " := ((P : UPred ()) k tt) (at level 60, no associativity).
@@ -179,20 +188,35 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 	The tactic wsatM is similar.
    *)
 
+  Lemma prefl {T} `{oT : preoType T} (t : T) : t ⊑ t. Proof. by reflexivity. Qed.
+  
+  Definition lerefl (n : nat) : n <= n. Proof. by reflexivity. Qed.
+  
+  Definition lt0 (n : nat) :  ~ n < 0. Proof. by omega. Qed.
+
+  Lemma propsMW {P w n r w'} (HSw : w ⊑ w') : P w n r -> P w' n r.
+  Proof. exact: (mu_mono _ _ P _ _ HSw). Qed.
+  
+  Lemma propsMNR {P w n r n' r'} (HLe : n' <= n) (HSr : r ⊑ r') : P w n r -> P w n' r'.
+  Proof. exact: (uni_pred _ _ _ _ _ HLe HSr). Qed.
+  
+  Lemma propsMN {P w n r n'} (HLe : n' <= n) : P w n r -> P w n' r.
+  Proof. apply: (propsMNR HLe (prefl r)). Qed.
+  
+  Lemma propsMR {P w n r r'} (HSr : r ⊑ r') : P w n r -> P w n r'.
+  Proof. exact: (propsMNR (lerefl n) HSr). Qed.
+  
   Lemma propsM {P w n r w' n' r'}
       (HP : P w n r) (HSw : w ⊑ w') (HLe : n' <= n) (HSr : r ⊑ r') :
     P w' n' r'.
-  Proof. by apply: (mu_mono _ _ P _ _ HSw); exact: (uni_pred _ _ _ _ _ HLe HSr). Qed.
+  Proof. by apply: (propsMW HSw); exact: (propsMNR HLe HSr). Qed.
 
   Ltac propsM H := solve [ done | apply (propsM H); solve [ done | reflexivity | omega ] ].
 
-  Lemma wsatM {σ m} {r : res} {w n k}
-      (HW : wsat σ m r w @ n) (HLe : k <= n) :
-    wsat σ m r w @ k.
+  Lemma wsatM {σ m} {r : res} {w n k} (HLe : k <= n) :
+    wsat σ m r w @ n -> wsat σ m r w @ k.
   Proof. by exact: (uni_pred _ _ _ _ _ HLe). Qed.
 
-  Ltac wsatM H := solve [done | apply (wsatM H); solve [done | omega] ].
-
   Section ViewShifts.
     Local Obligation Tactic := intros.
 
@@ -444,6 +468,9 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
   End HoareTriples.
 
+  (* Simple things, needed elsewhere. *)
+  Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
+
 End IRIS_PLOG.
 
 Module IrisPlog (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) : IRIS_PLOG RL C R WP CORE.
diff --git a/lang.v b/lang.v
index 12dd6eecf386a2ad9b9b85363de3cec978c14b0e..b95a99e515980e9c5d18d14721786ed6fd95461c 100644
--- a/lang.v
+++ b/lang.v
@@ -1,3 +1,4 @@
+Require Import ssreflect.
 Require Import List.
 Require Import core_lang.
 
@@ -5,6 +6,8 @@ Require Import core_lang.
 (** * Derived language with threadpool steps **)
 (******************************************************************)
 
+Set Bullet Behavior "Strict Subproofs".
+
 Module Lang (C : CORE_LANG).
 
   Export C.
@@ -58,7 +61,7 @@ Module Lang (C : CORE_LANG).
   Proof.
     intros HEq.
     apply fill_inj1 with (K [[ fork_ret ]]).
-    now rewrite !fill_comp, HEq.
+    now rewrite -> !fill_comp, HEq.
   Qed.
 
   Lemma comp_ctx_inj2  K K1 K2 :
@@ -67,7 +70,7 @@ Module Lang (C : CORE_LANG).
   Proof.
     intros HEq.
     apply fill_inj1 with fork_ret, fill_inj2 with K.
-    now rewrite !fill_comp, HEq.
+    now rewrite -> !fill_comp, HEq.
   Qed.
 
   Lemma comp_ctx_neut_emp_r K K' :
@@ -97,6 +100,14 @@ Module Lang (C : CORE_LANG).
     now erewrite fill_empty.
   Qed.
 
+  Lemma reducible_not_fork {e K e'} :
+    reducible e -> e <> K [[fork e']].
+  Proof.
+    move=> HRed HDec.
+    move: (fork_stuck K e'); rewrite -HDec -(fill_empty e) => HStuck {HDec}.
+    exact: (HStuck _ _ eq_refl).
+  Qed.
+
   Lemma step_same_ctx: forall K K' e e',
                          fill K e = fill K' e' ->
                          reducible e  ->
diff --git a/lib/ModuRes/BI.v b/lib/ModuRes/BI.v
index 87d1927bebdd6551de14676d9272c585c45e0e87..05b4b836a7a49e3a20eea5170fba7df54350ab27 100644
--- a/lib/ModuRes/BI.v
+++ b/lib/ModuRes/BI.v
@@ -111,10 +111,10 @@ Notation "p ∨ q" := (or p q) (at level 50, left associativity) : bi_scope.
 Notation "p * q" := (sc p q) (at level 40, left associativity) : bi_scope.
 Notation "p → q" := (impl p q) (at level 55, right associativity) : bi_scope.
 Notation "p '-*' q" := (si p q) (at level 55, right associativity) : bi_scope.
-Notation "∀ x , p" := (all n[(fun x => p)]) (at level 60, x ident, no associativity) : bi_scope.
-Notation "∃ x , p" := (xist n[(fun x => p)]) (at level 60, x ident, no associativity) : bi_scope.
-Notation "∀ x : T , p" := (all n[(fun x : T => p)]) (at level 60, x ident, no associativity) : bi_scope.
-Notation "∃ x : T , p" := (xist n[(fun x : T => p)]) (at level 60, x ident, no associativity) : bi_scope.
+Notation "∀ x , p" := (all n[(fun x => p)]) (at level 60, x ident, right associativity) : bi_scope.
+Notation "∃ x , p" := (xist n[(fun x => p)]) (at level 60, x ident, right associativity) : bi_scope.
+Notation "∀ x : T , p" := (all n[(fun x : T => p)]) (at level 60, x ident, right associativity) : bi_scope.
+Notation "∃ x : T , p" := (xist n[(fun x : T => p)]) (at level 60, x ident, right associativity) : bi_scope.
 
 Require Import UPred.
 
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 6a848f2801967fa40cf4aef83a1c77b297c50a9b..516e15127d15584d0d07b23d9a0b915bd62363de 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -1,11 +1,14 @@
 (** Resource algebras: Commutative monoids with a validity predicate. *)
 
+Require Import ssreflect.
 Require Import Bool.
 Require Import Predom.
 Require Import CSetoid.
 Require Import MetricCore.
 Require Import PreoMet.
 
+Set Bullet Behavior "Strict Subproofs".
+
 Class Associative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
   assoc : forall t1 t2 t3, op t1 (op t2 t3) == op (op t1 t2) t3.
 Class Commutative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
@@ -47,7 +50,7 @@ Section RAs.
   Proof.
     rewrite comm. now eapply ra_op_unit.
   Qed.
-  
+
   Lemma ra_op_valid2 t1 t2: ↓ (t1 · t2) -> ↓ t2.
   Proof.
     rewrite comm. now eapply ra_op_valid.
@@ -64,6 +67,15 @@ Section RAs.
   Proof.
     rewrite comm. now eapply ra_op_invalid.
   Qed.
+
+  (* PDS: The duplication is ugly, but ra_op_valid2 fails (slowly), and ra_opV2 does not and I haven't looked into it. *)
+
+  Lemma ra_opV1 {t t'} (Hv : ↓(t · t')) : ↓t.
+  Proof. exact: ra_op_valid. Qed.
+
+  Lemma ra_opV2 {t t'} (Hv : ↓(t · t')) : ↓t'.
+  Proof. by move: Hv; rewrite comm; exact: ra_op_valid. Qed.
+
 End RAs.
 
 (* RAs with cartesian products of carriers. *)
@@ -83,12 +95,12 @@ Section Products.
   Proof.
     split.
     - intros [s1 t1] [s2 t2] [Heqs Heqt]. intros [s'1 t'1] [s'2 t'2] [Heqs' Heqt']. simpl in *.
-      split; [rewrite Heqs, Heqs'|rewrite Heqt, Heqt']; reflexivity.
+      split; [rewrite -> Heqs, Heqs'|rewrite ->Heqt, Heqt']; reflexivity.
     - intros [s1 t1] [s2 t2] [s3 t3]. simpl; split; now rewrite ra_op_assoc.
     - intros [s1 t1] [s2 t2]. simpl; split; now rewrite ra_op_comm.
     - intros [s t]. simpl; split; now rewrite ra_op_unit.
     - intros [s1 t1] [s2 t2] [Heqs Heqt]. unfold ra_valid; simpl in *.
-      rewrite Heqs, Heqt. reflexivity.
+      rewrite -> Heqs, Heqt. reflexivity.
     - unfold ra_unit, ra_valid; simpl. split; eapply ra_valid_unit; now apply _.
     - intros [s1 t1] [s2 t2]. unfold ra_valid; simpl. intros [H1 H2]. split.
       + eapply ra_op_valid; now eauto.
@@ -98,13 +110,13 @@ End Products.
 
 Section ProductLemmas.
   Context {S T} `{raS : RA S, raT : RA T}.
-    
+
   Lemma ra_op_prod_fst (st1 st2: S*T):
     fst (st1 · st2) = fst st1 · fst st2.
   Proof.
     destruct st1 as [s1 t1]. destruct st2 as [s2 t2]. reflexivity.
   Qed.
-  
+
   Lemma ra_op_prod_snd (st1 st2: S*T):
     snd (st1 · st2) = snd st1 · snd st2.
   Proof.
@@ -133,14 +145,14 @@ Section Order.
     - intros z yz xyz [y Hyz] [x Hxyz]; exists (x · y).
       rewrite <- Hxyz, <- Hyz; symmetry; apply assoc.
   Qed.
-  
+
   Global Program Instance ra_preo : preoType T := mkPOType ra_ord.
 
   Global Instance equiv_pord_ra : Proper (equiv ==> equiv ==> equiv) (pord (T := T)).
   Proof.
     intros s1 s2 EQs t1 t2 EQt; split; intros [s HS].
     - exists s; rewrite <- EQs, <- EQt; assumption.
-    - exists s; rewrite EQs, EQt; assumption.
+    - exists s; rewrite -> EQs, EQt; assumption.
   Qed.
 
   Global Instance ra_op_monic : Proper (pord ++> pord ++> pord) (ra_op _).
@@ -149,6 +161,13 @@ Section Order.
     rewrite <- assoc, (comm y), <- assoc, assoc, (comm y1), EQx, EQy; reflexivity.
   Qed.
 
+  Global Program Instance ra_valid_ord : Proper (pord ==> flip impl) ra_valid.
+  Next Obligation.
+    move=>r r' [r'' HLe] Hv.
+    move: Hv; rewrite -HLe => {HLe}.
+    exact: ra_op_valid2.
+  Qed.
+
   Lemma unit_min r : 1 ⊑ r.
   Proof.
     exists r. simpl.
@@ -159,7 +178,7 @@ End Order.
 
 Section Exclusive.
   Context (T: Type) `{Setoid T}.
-  
+
   Inductive ra_res_ex: Type :=
   | ex_own: T -> ra_res_ex
   | ex_unit: ra_res_ex
@@ -186,7 +205,7 @@ Section Exclusive.
 
   Global Program Instance ra_type_ex : Setoid ra_res_ex :=
     mkType ra_res_ex_eq.
-      
+
   Global Instance ra_unit_ex : RA_unit ra_res_ex := ex_unit.
   Global Instance ra_op_ex : RA_op ra_res_ex :=
     fun r s =>
@@ -201,11 +220,11 @@ Section Exclusive.
                | ex_bot => False
                | _      => True
              end.
-  
+
   Global Instance ra_ex : RA ra_res_ex.
   Proof.
     split.
-    - intros [t1| |] [t2| |] Heqt [t'1| |] [t'2| |] Heqt'; simpl; now auto.  
+    - intros [t1| |] [t2| |] Heqt [t'1| |] [t'2| |] Heqt'; simpl; now auto.
     - intros [s1| |] [s2| |] [s3| |]; reflexivity.
     - intros [s1| |] [s2| |]; reflexivity.
     - intros [s1| |]; reflexivity.
@@ -220,19 +239,19 @@ End Exclusive.
 Section Agreement.
   Context T `{T_ty : Setoid T} (eq_dec : forall x y, {x == y} + {x =/= y}).
   Local Open Scope ra_scope.
-  
+
   Inductive ra_res_agree : Type :=
     | ag_bottom
     | ag_unit
     | ag_inj (t : T).
-  
+
   Global Instance ra_unit_agree : RA_unit _ := ag_unit.
-  Global Instance ra_valid_ag : RA_valid _ := 
+  Global Instance ra_valid_ag : RA_valid _ :=
            fun x => match x with ag_bottom => False | _ => True end.
   Global Instance ra_op_ag : RA_op _ :=
     fun x y => match x, y with
-               | ag_inj t1, ag_inj t2 => 
-                   if eq_dec t1 t2 then ag_inj t1 else ag_bottom
+               | ag_inj t1, ag_inj t2 =>
+                   if eq_dec t1 t2 is left _ then ag_inj t1 else ag_bottom
                | ag_bottom , y => ag_bottom
                | x , ag_bottom => ag_bottom
                | ag_unit, y => y
@@ -240,14 +259,14 @@ Section Agreement.
              end.
 
   Definition ra_eq_ag (x : ra_res_agree) (y : ra_res_agree) : Prop :=
-    match x,y with 
+    match x,y with
       | ag_inj t1, ag_inj t2 => t1 == t2
       | x, y => x = y
     end.
-  
+
 
   Global Instance ra_equivalence_agree : Equivalence ra_eq_ag.
-  Proof. 
+  Proof.
     split; intro; intros; destruct x; try (destruct y; try destruct z); simpl; try reflexivity;
     simpl in *; try inversion H; try inversion H0; try rewrite <- H; try rewrite <- H0; try firstorder.
   Qed.
@@ -255,29 +274,29 @@ Section Agreement.
   Global Instance res_agree : RA ra_res_agree.
   Proof.
     split; repeat intro.
-    - repeat (match goal with [ x : ra_res_agree |- _ ] => destruct x end); 
+    - repeat (match goal with [ x : ra_res_agree |- _ ] => destruct x end);
       simpl in *; try reflexivity; try rewrite H; try rewrite H0; try reflexivity;
       try inversion H; try inversion H0; compute;
       destruct (eq_dec t2 t0), (eq_dec t1 t); simpl; auto; exfalso;
       [ rewrite <- H, -> e in c | rewrite -> H, -> e in c; symmetry in c]; contradiction.
-    - repeat (match goal with [ x : ra_res_agree |- _ ] => destruct x end); 
+    - repeat (match goal with [ x : ra_res_agree |- _ ] => destruct x end);
       simpl in *; auto; try reflexivity; compute; try destruct (eq_dec _ _); try reflexivity.
       destruct (eq_dec t0 t), (eq_dec t1 t0), (eq_dec t1 t); simpl; auto; try reflexivity;
-      rewrite e in e0; contradiction.
-    -  destruct t1, t2; try reflexivity; compute; destruct (eq_dec t0 t), (eq_dec t t0); 
+      rewrite -> e in e0; contradiction.
+    -  destruct t1, t2; try reflexivity; compute; destruct (eq_dec t0 t), (eq_dec t t0);
        try reflexivity; auto; try contradiction; symmetry in e; contradiction.
     - destruct t; reflexivity.
     - destruct x, y; simpl; firstorder; now inversion H.
     - now constructor.
     - destruct t1, t2; try contradiction; now constructor.
-  Qed. 
+  Qed.
 
 End Agreement.
 
 
 Section InfiniteProduct.
   (* I is the index type (domain), S the type of the components (codomain) *)
-  Context (I : Type) (S : forall (i : I), Type) 
+  Context (I : Type) (S : forall (i : I), Type)
           {tyS : forall i, Setoid (S i)}
           {uS : forall i, RA_unit (S i)}
           {opS : forall i, RA_op (S i)}
@@ -288,22 +307,22 @@ Section InfiniteProduct.
   Definition ra_res_infprod := forall (i : I), S i.
 
   Implicit Type (i : I) (f g : ra_res_infprod).
-  
+
   Definition ra_eq_infprod := fun f g => forall i, f i == g i.
   Global Instance ra_equiv_infprod : Equivalence ra_eq_infprod.
-  Proof. split; repeat intro; [ | rewrite (H i) | rewrite (H i), (H0 i) ]; reflexivity. Qed.
-  
+  Proof. split; repeat intro; [ | rewrite (H i) | rewrite -> (H i), (H0 i) ]; reflexivity. Qed.
+
   Global Instance ra_type_infprod : Setoid ra_res_infprod | 5 := mkType ra_eq_infprod.
   Global Instance ra_unit_infprod : RA_unit _ := fun i => ra_unit (S i).
   Global Instance ra_op_infprod : RA_op _ := fun f g i => f i · g i.
-  Global Instance ra_valid_infprod : RA_valid _ := fun f => forall i, ra_valid (f i). 
+  Global Instance ra_valid_infprod : RA_valid _ := fun f => forall i, ra_valid (f i).
   Global Instance ra_infprod : RA ra_res_infprod.
   Proof.
     split; repeat intro.
     - eapply ra_op_proper; [ now auto | | ]; now firstorder.
-    - compute; now rewrite (ra_op_assoc (RA := raS i) _ (t1 i) (t2 i) (t3 i)). 
-    - compute; now rewrite (ra_op_comm (RA := raS i) _ (t1 i) (t2 i)).
-    - compute; now rewrite (ra_op_unit (RA := raS i) _ (t i)).
+    - compute; now rewrite -> (ra_op_assoc (RA := raS i) _ (t1 i) (t2 i) (t3 i)).
+    - compute; now rewrite -> (ra_op_comm (RA := raS i) _ (t1 i) (t2 i)).
+    - compute; now rewrite -> (ra_op_unit (RA := raS i) _ (t i)).
     - compute; intros; split; intros; symmetry in H;
       eapply (ra_valid_proper (RA := raS i) _ _ _ (H i)); now firstorder.
     - now eapply (ra_valid_unit (RA := raS i) _).
@@ -315,7 +334,7 @@ End InfiniteProduct.
 Section HomogeneousProduct.
   (* I is the index type (domain), S the type of the components (codomain) *)
   Context (I : Type) (S : Type) `{RA S}.
-  
+
   Global Instance ra_homprod : RA (forall (i : I), S).
   Proof. now eapply ra_infprod; auto. Qed.
 End HomogeneousProduct.