diff --git a/iris.v b/iris.v
index b943f6120389de543ec6fb59f282de507b7b971d..bef92ebde55cd3ea5d1a6905f483283ae7256b40 100644
--- a/iris.v
+++ b/iris.v
@@ -4,7 +4,7 @@ Require Import RecDom.PCM RecDom.UPred RecDom.BI RecDom.PreoMet RecDom.Finmap.
 Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
 
   Module Import L  := Lang RP RL C.
-  Module R <: PCM_T.
+  Module Import R <: PCM_T.
     Definition res := (RP.res * RL.res)%type.
     Instance res_op   : PCM_op res := _.
     Instance res_unit : PCM_unit res := _.
@@ -12,8 +12,6 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
   End R.
   Module Import WP := WorldProp R.
 
-  Definition res := option R.res.
-
   Delimit Scope iris_scope with iris.
   Local Open Scope iris_scope.
 
@@ -37,7 +35,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
     Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
 
     Program Definition box : Props -n> Props :=
-      n[(fun p => m[(fun w => mkUPred (fun n r => p w n 1%pcm) _)])].
+      n[(fun p => m[(fun w => mkUPred (fun n r => p w n (pcm_unit _)) _)])].
     Next Obligation.
       intros n m r s HLe _ Hp; rewrite HLe; assumption.
     Qed.
@@ -66,7 +64,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
       intros n1 n2 _ _ HLe _; apply mono_dist; now auto with arith.
     Qed.
 
-    Program Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).
+    Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).
 
     Instance intEq_equiv : Proper (equiv ==> equiv ==> equiv) intEqP.
     Proof.
@@ -126,23 +124,6 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
 
   End Invariants.
 
-  (** Ownership **)
-  Definition own (r : res) : Props :=
-    pcmconst (up_cr (pord r)).
-
-  Definition injFst (r : option RP.res) : res :=
-    option_map (fun r => (r, pcm_unit _)) r.
-  Definition injSnd (r : option RL.res) : res :=
-    option_map (fun r => (pcm_unit _, r)) r.
-
-  (** Physical part **)
-  Definition ownP (r : RP.res) : Props :=
-    own (injFst (Some r)).
-
-  (** Logical part **)
-  Definition ownL (r : RL.res) : Props :=
-    own (injSnd (Some r)).
-
   Notation "â–¡ p" := (box p) (at level 30, right associativity) : iris_scope.
   Notation "⊤" := (top : Props) : iris_scope.
   Notation "⊥" := (bot : Props) : iris_scope.
@@ -156,64 +137,82 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
   Notation "∀ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
   Notation "∃ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
 
+  (** Ownership **)
+  Definition ownR (r : res) : Props :=
+    pcmconst (up_cr (pord r)).
+
+  (** Physical part **)
+  Definition ownRP (r : RP.res) : Props :=
+    ownR (r, pcm_unit _).
+
+  (** Logical part **)
+  Definition ownRL (r : RL.res) : Props :=
+    ownR (pcm_unit _, r).
+
+  (** Proper ghost state: ownership of logical w/ possibility of undefined **)
+  Definition ownL (r : option RL.res) : Props :=
+    match r with
+      | Some r => ownRL r
+      | None => ⊥
+    end.
+
   Section Erasure.
     Local Open Scope pcm_scope.
     Local Open Scope bi_scope.
-    Local Instance eqRes : Setoid res := discreteType.
 
     (* First, we need to erase a finite map. This won't be pretty, for
        now, since the library does not provide enough
        constructs. Hopefully we can provide a fold that'd work for
        that at some point
      *)
-    Fixpoint comp_list (xs : list res) : res :=
+    Fixpoint comp_list (xs : list res) : option res :=
       match xs with
         | nil => 1
-        | (x :: xs)%list => x · comp_list xs
+        | (x :: xs)%list => Some x · comp_list xs
       end.
 
     Definition cod (m : nat -f> res) : list res := List.map snd (findom_t m).
-    Definition erase (m : nat -f> res) : res := comp_list (cod m).
+    Definition erase (m : nat -f> res) : option res := comp_list (cod m).
 
     Lemma erase_remove (rs : nat -f> res) i r (HLu : rs i = Some r) :
-      erase rs = r · erase (fdRemove i rs).
+      erase rs == Some r · erase (fdRemove i rs).
     Proof.
-      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl in *.
-      induction rs as [| [j s] ]; [discriminate |]; simpl in *.
+      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
+      induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
       destruct (comp i j); [inversion HLu; reflexivity | discriminate |].
-      simpl; rewrite IHrs by eauto using SS_tail.
-      rewrite !assoc; f_equal; rewrite comm; reflexivity.
+      simpl comp_list; rewrite IHrs by eauto using SS_tail.
+      rewrite !assoc, (comm (Some s)); reflexivity.
     Qed.
 
     Lemma erase_insert_new (rs : nat -f> res) i r (HNLu : rs i = None) :
-      r · erase rs = erase (fdUpdate i r rs).
+      Some r · erase rs == erase (fdUpdate i r rs).
     Proof.
-      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl in *.
-      induction rs as [| [j s] ]; simpl in *; [reflexivity |].
+      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
+      induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
       destruct (comp i j); [discriminate | reflexivity |].
-      simpl; rewrite <- IHrs by eauto using SS_tail.
-      rewrite !assoc; f_equal; rewrite comm; reflexivity.
+      simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
+      rewrite !assoc, (comm (Some r)); reflexivity.
     Qed.
 
-    Lemma erase_insert_old (rs : nat -f> res) i r1 r2 (HLu : rs i = Some r1) :
-      r2 · erase rs = erase (fdUpdate i (r1 · r2) rs).
+    Lemma erase_insert_old (rs : nat -f> res) i r1 r2 r
+          (HLu : rs i = Some r1) (HEq : Some r1 · Some r2 == Some r) :
+      Some r2 · erase rs == erase (fdUpdate i r rs).
     Proof.
-      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl in *.
-      induction rs as [| [j s] ]; [discriminate |]; simpl in *.
+      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
+      induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
       destruct (comp i j); [inversion HLu; subst; clear HLu | discriminate |].
-      - simpl; rewrite assoc, (comm r2); reflexivity.
-      - simpl; rewrite <- IHrs by eauto using SS_tail.
-        rewrite !assoc, (comm r2); reflexivity.
+      - simpl comp_list; rewrite assoc, (comm (Some r2)), <- HEq; reflexivity.
+      - simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
+        rewrite !assoc, (comm (Some r2)); reflexivity.
     Qed.
 
     Global Instance preo_unit : preoType () := disc_preo ().
 
-    (* XXX: logical state omitted, since it looks weird. Also, later over the whole deal. *)
     Program Definition erasure (σ : state) (m : mask) (r s : res) (w : Wld) : UPred () :=
       â–¹ (mkUPred (fun n _ =>
-                    erase_state (option_map fst (r · s)) σ
+                    erase_state (option_map fst (Some r · Some s)) σ
                     /\ exists rs : nat -f> res,
-                         erase rs = s /\
+                         erase rs == Some s /\
                          forall i (Hm : m i),
                            (i ∈ dom rs <-> i ∈ dom w) /\
                            forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
@@ -263,22 +262,26 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
     Local Open Scope mask_scope.
     Local Open Scope pcm_scope.
     Local Obligation Tactic := intros.
-    Local Existing Instance eqRes.
 
     Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
-      mkUPred (fun n r => forall w1 s rf mf σ k (HSub : w ⊑ w1) (HLe : k <= n)
-                                 (HGt : k > 0) (HD : mf # m1 ∪ m2)
-                                 (HE : erasure σ (m1 ∪ mf) (r · rf) s w1 @ k),
-                          exists w2 r' s', w1 ⊑ w2 /\ p w2 k r' /\
-                                           erasure σ (m2 ∪ mf) (r' · rf) s' w2 @ k) _.
+      mkUPred (fun n r => forall w1 rf rr s mf σ k (HSub : w ⊑ w1) (HLe : k < n)
+                                 (HD : mf # m1 ∪ m2) (HEq : Some r · Some rf == Some rr)
+                                 (HE : erasure σ (m1 ∪ mf) rr s w1 @ S k),
+                          exists w2 r' rr' s',
+                            w1 ⊑ w2 /\ p w2 (S k) r' /\ Some r' · Some rf == Some rr'
+                            /\ erasure σ (m2 ∪ mf) rr' s' w2 @ S k) _.
     Next Obligation.
       intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
-      destruct (HP w1 s (rd · rf) mf σ k) as [w2 [r1' [s' [HW [HP' HE'] ] ] ] ]; try assumption; [| |].
-      - etransitivity; eassumption.
-      - rewrite assoc, (comm r1), HR; assumption.
-      - exists w2 (rd · r1') s'; split; [assumption | split].
-        + eapply uni_pred, HP'; [| eexists]; reflexivity.
-        + rewrite (comm rd), <- assoc; assumption.
+      rewrite <- HR, (comm (Some rd)), <- assoc in HEq; clear r2 HR.
+      destruct (Some rd · Some rf) as [rf' |] eqn: HR;
+        [| erewrite comm, pcm_op_zero in HEq by apply _; contradiction].
+      destruct (HP w1 rf' rr s mf σ k) as [w2 [r1' [rr' [s' [HW [HP' [HR' HE'] ] ] ] ] ] ]; try assumption; [|].
+      - eauto with arith.
+      - rewrite <- HR, assoc in HR'; clear rf' HR HEq HP.
+        destruct (Some r1' · Some rd) as [r2' |] eqn: HR;
+          [| erewrite pcm_op_zero in HR' by apply _; contradiction].
+        exists w2 r2' rr' s'; split; [assumption | split; [| split; assumption] ].
+        eapply uni_pred, HP'; [| exists rd; rewrite comm, HR]; reflexivity.
     Qed.
 
     Program Definition pvs (m1 m2 : mask) : Props -n> Props :=
@@ -294,19 +297,19 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
       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' [rr' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ].
         + eapply erasure_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'; repeat split; [assumption | |].
+          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR HE'] ];
+          exists (extend w1'' w2') r' rr' s'; split; [assumption | split; [| split; [assumption |] ] ].
           * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
           * eapply erasure_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' [rr' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ].
         + eapply erasure_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'; repeat split; [assumption | |].
+          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR HE'] ];
+          exists (extend w1'' w2') r' rr' s'; split; [assumption | split; [| split; [assumption |] ] ].
           * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
           * eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
     Qed.
@@ -321,11 +324,11 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
     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; [].
-        clear HP; repeat eexists; try eassumption; [].
+      - edestruct HP as [w2 [r' [rr' [s' [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; [].
-        clear HP; repeat eexists; try eassumption; [].
+      - edestruct HP as [w2 [r' [rr' [s' [HW [HP' HE'] ] ] ] ] ]; try eassumption; [].
+        clear HP; repeat (eexists; try eassumption); [].
         apply EQp; [now eauto with arith | assumption].
     Qed.
 
@@ -338,7 +341,8 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
     Local Open Scope mask_scope.
     Local Open Scope pcm_scope.
     Local Open Scope bi_scope.
-    Local Existing Instance eqRes.
+
+    Implicit Types (p q r : Props) (i : nat) (m : mask).
 
     Definition mask_sing i := mask_set mask_emp i True.
 
@@ -351,18 +355,33 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
       apply ı in HInv; rewrite (isoR p) in HInv.
       (* get rid of the invisible 1/2 *)
       do 8 red in HInv.
-      destruct k as [| k]; [now inversion HGt |].
       destruct HE as [HES [rs [HE HM] ] ].
       destruct (rs i) as [ri |] eqn: HLr.
-      - exists w' (r · ri) (erase (fdRemove i rs)); split; [reflexivity | split; [| split] ].
+      - rewrite erase_remove with (i := i) (r := ri) in HE by assumption.
+        destruct (Some rr · Some s) as [ss |] eqn: HR; setoid_rewrite HR in HES;
+          [| contradiction (erase_state_nonzero _ HES) ].
+        destruct (Some r · Some rf) as [rr' |] eqn: HR1;
+          [simpl in HEq; subst rr' | contradiction].
+        destruct (Some ri · erase (fdRemove i rs)) as [s' |] eqn: HR2;
+          [simpl in HE; subst s' | contradiction].
+        assert (HEq : Some r · Some ri · Some rf · erase (fdRemove i rs) == Some ss).
+        { rewrite <- (assoc (Some r)), (comm (Some ri)), assoc, HR1, <- assoc, HR2, HR; reflexivity. }
+        clear HR HR1 HR2; destruct (Some r · Some ri) as [rri |] eqn: HR1;
+        [| now erewrite !pcm_op_zero in HEq by apply _].
+        destruct (Some rri · Some rf) as [rr' |] eqn: HR2;
+          [| now erewrite pcm_op_zero in HEq by apply _].
+        destruct (erase (fdRemove i rs)) as [s' |] eqn: HRS;
+          [| now erewrite comm, pcm_op_zero in HEq by apply _].
+        exists w' rri rr' s'; split; [reflexivity | split; [| split; [rewrite HR2; reflexivity | split] ] ].
         + simpl; eapply HInv; [now auto with arith |].
           specialize (HSub i); rewrite HLu in HSub.
-          eapply uni_pred, HM with i; [| exists r | | | rewrite HLr]; try reflexivity; [|].
+          eapply uni_pred, HM with i; [| exists r; rewrite <- HR1 | | | rewrite HLr]; try reflexivity; [|].
           * left; unfold mask_sing, mask_set.
             destruct (Peano_dec.eq_nat_dec i i); tauto.
           * symmetry; destruct (w' i); [assumption | contradiction].
-        + rewrite <- assoc, (comm ri), assoc, <- (assoc _ ri), <- erase_remove, HE; assumption.
-        + exists (fdRemove i rs); split; [reflexivity | intros j Hm].
+        + destruct (Some rr' · Some s') as [ss' |] eqn: HR; [| contradiction].
+          setoid_rewrite HR; simpl in HEq; subst; assumption.
+        + exists (fdRemove i rs); split; [rewrite HRS; reflexivity | 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].
@@ -374,10 +393,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
         destruct (Peano_dec.eq_nat_dec i i); tauto.
     Qed.
 
-    (* XXX: move up *)
-    Implicit Types (p q r : Props) (i : nat) (m : mask).
-
-    Lemma vsClose i p :
+    (*Lemma vsClose i p :
       valid (vs mask_emp (mask_sing i) (inv i p * ▹ p) ⊤).
     Proof.
       intros pw nn r w _; clear r pw.
@@ -410,39 +426,43 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
             subst r; rewrite assoc; eexists; reflexivity.
         + rewrite fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption.
           auto.
-    Qed.
+    Qed.*)
 
     Lemma vsTrans p q r m1 m2 m3 (HMS : m2 ⊆ m1 ∪ m3) :
       vs m1 m2 p q ∧ vs m2 m3 q r ⊑ vs m1 m3 p r.
     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 [rrq [sq [HSw12 [Hq [HEq' HErq] ] ] ] ] ] ]; try eassumption; [|].
       { (* XXX: possible lemma *)
         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 : 1 ⊑ rq) by (exists rq; rewrite comm; apply pcm_op_unit, _).
+      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 k _ HLe0 HS Hq w2) as [w3 [rr [sr [HSw23 [Hr HEr] ] ] ] ];
-        try (reflexivity || eassumption); [|].
+      edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [rrR [sR [HSw23 [Hr [HR HEr] ] ] ] ] ] ];
+        try (reflexivity || eassumption); [now auto with arith | |].
       { (* XXX: possible lemma *)
         clear - HD HMS.
         intros j [Hmf Hm23]; apply (HD j); split; [assumption |].
         destruct Hm23 as [Hm2 | Hm3]; [apply HMS, Hm2 | right; assumption].
       }
       clear HEq Hq HS.
-      setoid_rewrite HSw12; eauto 6.
+      setoid_rewrite HSw12; eauto 8.
     Qed.
 
-    (* Warning: weak statement *)
-    Lemma vsEnt p q m1 m2 (HEnt : p ⊑ q) :
-      valid (vs m1 m2 p q).
+    Lemma vsEnt p q m :
+      □ (p → q) ⊑ vs m m p q.
     Proof.
-    Admitted.
+      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 rr s; split; [reflexivity | split; [| 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.
 
-    Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1 ∪ m2) :
+    (* Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1 ∪ m2) :
       vs m1 m2 p q ⊑ vs (m1 ∪ mf) (m2 ∪ mf) (p * r) (q * r).
     Proof.
       intros w' n r1 HVS w HSub; specialize (HVS _ HSub); clear w' r1 HSub.
@@ -459,7 +479,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
         + rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr; now auto.
         + rewrite <- assoc; eapply erasure_equiv, HEq; try reflexivity; [].
           clear; intros i; tauto.
-    Qed.
+    Qed.*)
 
     Lemma vsFalse m1 m2 :
       valid (vs m1 m2 ⊥ ⊥).
@@ -478,48 +498,66 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
     Local Open Scope pcm_scope.
     Local Open Scope bi_scope.
     Local Open Scope lang_scope.
-    Local Existing Instance eqRes.
 
     Global Instance expr_type : Setoid expr := discreteType.
     Global Instance expr_metr : metric expr := discreteMetric.
+    Global Instance expr_cmetr : cmetric expr := discreteCMetric.
+    Instance LP_isval : LimitPreserving is_value.
+    Proof.
+      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).
 
     Local Obligation Tactic := intros; eauto with typeclass_instances.
 
     Definition wpFP m (WP : expr -n> (value -n> Props) -n> Props) e φ w n r :=
-      forall w' k s rf σ (HSw : w ⊑ w') (HLt : k < n)
-             (HE : erasure σ m (r · rf) s w' @ S k),
+      forall w' k s rf rr σ
+             (HSw : w ⊑ w') (HLt : k < n) (HR : Some r · Some rf == Some rr)
+             (HE : erasure σ m rr s w' @ S k),
         (forall (HV : is_value e),
-         exists w'' r' s', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
-                           /\ erasure σ m (r' · rf) s' w'' @ S k) /\
+         exists w'' r' rr' s', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
+                               /\ Some r' · Some rf == Some rr'
+                               /\ erasure σ m rr' s' 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'
-                           /\ erasure σ' m (r' · rf) s' w'' @ k) /\
+         exists w'' r' rr' s', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
+                               /\ Some r' · Some rf == Some rr'
+                               /\ erasure σ' m rr' s' w'' @ k) /\
         (forall e' K (HDec : e = K [[ e' ]]),
-         exists w'' rfk rret s', w' ⊑ w'' /\ erasure σ m (rfk · rret · rf) s' w'' @ k
-                                 /\ WP (K [[ fork_ret ]]) φ w'' k rret
-                                 /\ WP e' (umconst ⊤) w'' k rfk).
+         exists w'' rfk rret rr' s', w' ⊑ w'' /\ Some rfk · Some rret · Some rf == Some rr'
+                                     /\ WP (K [[ fork_ret ]]) φ w'' k rret
+                                     /\ WP e' (umconst ⊤) w'' k rfk
+                                     /\ erasure σ m rr' s' w'' @ k).
 
     Program Definition wpF 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 m WP e φ w) _)])])])].
     Next Obligation.
-      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf σ HSw HLt HE.
-      specialize (Hp w' k s (rd · rf) σ); destruct Hp as [HV [HS HF] ];
-      [assumption | now eauto with arith | rewrite assoc, (comm r1), EQr; assumption |].
+      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf rr σ HSw HLt HR HE.
+      rewrite <- EQr, (comm (Some rd)), <- assoc in HR.
+      destruct (Some rd · Some rf) as [rf' |] eqn: HRF;
+        [| now erewrite comm, pcm_op_zero in HR by apply _].
+      specialize (Hp w' k s rf' rr σ); destruct Hp as [HV [HS HF] ];
+      [| now eauto with arith | ..]; try assumption; [].
       split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
-      - specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ];
-        exists w'' (r' · rd) s'; split; [assumption | split; [| rewrite <- assoc; assumption] ].
-        eapply uni_pred, Hφ; [reflexivity | eexists; rewrite comm; reflexivity].
-      - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ];
-        exists w'' (r' · rd) s'; split; [assumption | split; [| rewrite <- assoc; assumption] ].
-        eapply uni_pred, HWP; [reflexivity | eexists; rewrite comm; reflexivity].
-      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HE' [HWR HWF] ] ] ] ] ] ];
-        exists w'' rfk (rret · rd) s'; split; [assumption | split; [| split] ].
-        + rewrite assoc in HE'; rewrite assoc; assumption.
-        + eapply uni_pred, HWR; [reflexivity | eexists; rewrite comm; reflexivity].
-        + assumption.
+      - specialize (HV HV0); destruct HV as [w'' [r2' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
+        rewrite <- HRF, assoc, (comm (Some r2')) in HR'.
+        destruct (Some rd · Some r2') as [r1' |] eqn: HR1;
+          [| now erewrite pcm_op_zero in HR' by apply _].
+        exists w'' r1' rr' s'; split; [assumption | split; [| split; assumption] ].
+        eapply uni_pred, Hφ; [| eexists; rewrite <- HR1]; reflexivity.
+      - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r2' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
+        rewrite <- HRF, assoc, (comm (Some r2')) in HR'.
+        destruct (Some rd · Some r2') as [r1' |] eqn: HR1;
+          [| now erewrite pcm_op_zero in HR' by apply _].
+        exists w'' r1' rr' s'; split; [assumption | split; [| split; assumption] ].
+        eapply uni_pred, HWP; [| eexists; rewrite <- HR1]; reflexivity.
+      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret2 [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+        rewrite <- HRF, assoc, <- (assoc (Some rfk)), (comm (Some rret2)) in HR'.
+        destruct (Some rd · Some rret2) as [rret1 |] eqn: HR1;
+          [| now erewrite (comm _ 0), !pcm_op_zero in HR' by apply _].
+        exists w'' rfk rret1 rr'; exists s'; repeat (split; try assumption); [].
+        eapply uni_pred, HWR; [| eexists; rewrite <- HR1]; reflexivity.
     Qed.
     Next Obligation.
       intros w1 w2 EQw n r; simpl.
@@ -533,46 +571,46 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
         edestruct (Hp (extend w2' w1)) as [HV [HS HF] ]; try eassumption;
         [eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
         split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
-        + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
+        + specialize (HV HV0); destruct HV as [w1'' [r' [rr' [s' [HSw'' [Hφ [HR' HE'] ] ] ] ] ] ].
           assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
           assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r' s'; split; [assumption |].
-          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
+          exists (extend w1'' w2') r' rr' s'; split; [assumption |].
+          split; [| split; [assumption | eapply erasure_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' [rr' [s' [HSw'' [HWP [HR' HE'] ] ] ] ] ] ].
           assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
           assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r' s'; split; [assumption |].
-          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
+          exists (extend w1'' w2') r' rr' s'; split; [assumption |].
+          split; [| split; [assumption | eapply erasure_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'' [HE' [HWR HWF] ] ] ] ] ] ].
+        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [rr' [s' [HSw'' [HR' [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 |].
-          split; [eapply erasure_dist, HE'; [eassumption | now eauto with arith] |].
-          split; eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
+          exists (extend w1'' w2') rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+          split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
+          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
       - assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
         edestruct (Hp (extend w2' w2)) as [HV [HS HF] ]; try eassumption;
         [eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
         split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
-        + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
+        + specialize (HV HV0); destruct HV as [w1'' [r' [rr' [s' [HSw'' [Hφ [HR' HE'] ] ] ] ] ] ].
           assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
           assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r' s'; split; [assumption |].
-          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
+          exists (extend w1'' w2') r' rr' s'; split; [assumption |].
+          split; [| split; [assumption | eapply erasure_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' [rr' [s' [HSw'' [HWP [HR' HE'] ] ] ] ] ] ].
           assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
           assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r' s'; split; [assumption |].
-          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
+          exists (extend w1'' w2') r' rr' s'; split; [assumption |].
+          split; [| split; [assumption | eapply erasure_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'' [HE' [HWR HWF] ] ] ] ] ] ].
+        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [rr' [s' [HSw'' [HR' [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 |].
-          split; [eapply erasure_dist, HE'; [eassumption | now eauto with arith] |].
-          split; eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
+          exists (extend w1'' w2') rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+          split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
+          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
     Qed.
     Next Obligation.
       intros w1 w2 Sw n r; simpl; intros Hp w'; intros; eapply Hp; try eassumption.
@@ -586,24 +624,24 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
       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] ]; try eassumption; [|].
       - 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' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
+          exists w'' r' rr' s'; split; [assumption | split; [| 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' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
+          exists w'' r' rr' s'; split; [assumption | split; [| 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' [HE' [HWR HWF] ] ] ] ] ] ].
-          exists w'' rfk rret s'; repeat (split; try assumption); [].
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+          exists w'' rfk rret rr'; exists s'; repeat (split; try assumption); [].
           eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | now eauto with arith].
       - 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' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
+          exists w'' r' rr' s'; split; [assumption | split; [| 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' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
+          exists w'' r' rr' s'; split; [assumption | split; [| 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' [HE' [HWR HWF] ] ] ] ] ] ].
-          exists w'' rfk rret s'; repeat (split; try assumption); [].
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+          exists w'' rfk rret rr'; exists s'; repeat (split; try assumption); [].
           eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | now eauto with arith].
     Qed.
     Next Obligation.
@@ -622,19 +660,19 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
       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] ]; try eassumption; [|].
       - split; [assumption | 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' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
+          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
           eapply (EQWP _ _ _), HWP; now eauto with arith.
-        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HE' [HWR HWF] ] ] ] ] ] ].
-          exists w'' rfk rret s'; split; [assumption | split; [assumption |] ].
-          split; eapply EQWP; try eassumption; now eauto with arith.
+        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+          exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
       - split; [assumption | 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' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
+          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
           eapply (EQWP _ _ _), HWP; now eauto with arith.
-        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HE' [HWR HWF] ] ] ] ] ] ].
-          exists w'' rfk rret s'; split; [assumption | split; [assumption |] ].
-          split; eapply EQWP; try eassumption; now eauto with arith.
+        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+          exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
     Qed.
 
     Instance contr_wpF m : contractive (wpF m).
@@ -642,19 +680,19 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
       intros n WP1 WP2 EQWP e φ w k r HLt.
       split; intros Hp w'; intros; edestruct Hp as [HV [HS HF] ]; try eassumption; [|].
       - split; [assumption | 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' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
+          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
           eapply EQWP, HWP; now eauto with arith.
-        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HE' [HWR HWF] ] ] ] ] ] ].
-          exists w'' rfk rret s'; split; [assumption | split; [assumption |] ].
-          split; eapply EQWP; try eassumption; now eauto with arith.
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+          exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
       - split; [assumption | 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' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
+          exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
           eapply EQWP, HWP; now eauto with arith.
-        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HE' [HWR HWF] ] ] ] ] ] ].
-          exists w'' rfk rret s'; split; [assumption | split; [assumption |] ].
-          split; eapply EQWP; try eassumption; now eauto with arith.
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+          exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
     Qed.
 
     Definition wp m : expr -n> (value -n> Props) -n> Props :=
diff --git a/lib/recdom/BI.v b/lib/recdom/BI.v
index 80b0964ed6832c99c9f18b2ad1e5dccdfbaefbf5..42de387d2df663883182f7a98def1722772b9a41 100644
--- a/lib/recdom/BI.v
+++ b/lib/recdom/BI.v
@@ -143,27 +143,25 @@ Section UPredBI.
   Context Res `{pcmRes : PCM Res}.
   Local Open Scope pcm_scope.
   Local Obligation Tactic := intros; eauto with typeclass_instances.
-  Local Existing Instance eqT.
-  Definition oRes := option Res.
 
   (* Standard interpretations of propositional connectives. *)
-  Global Program Instance top_up : topBI (UPred oRes) := up_cr (const True).
-  Global Program Instance bot_up : botBI (UPred oRes) := up_cr (const False).
+  Global Program Instance top_up : topBI (UPred Res) := up_cr (const True).
+  Global Program Instance bot_up : botBI (UPred Res) := up_cr (const False).
 
-  Global Program Instance and_up : andBI (UPred oRes) :=
+  Global Program Instance and_up : andBI (UPred Res) :=
     fun P Q =>
       mkUPred (fun n r => P n r /\ Q n r) _.
   Next Obligation.
     intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto.
   Qed.
-  Global Program Instance or_up : orBI (UPred oRes) :=
+  Global Program Instance or_up : orBI (UPred Res) :=
     fun P Q =>
       mkUPred (fun n r => P n r \/ Q n r) _.
   Next Obligation.
     intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto.
   Qed.
 
-  Global Program Instance impl_up : implBI (UPred oRes) :=
+  Global Program Instance impl_up : implBI (UPred Res) :=
     fun P Q =>
       mkUPred (fun n r => forall m r', m <= n -> r ⊑ r' -> P m r' -> Q m r') _.
   Next Obligation.
@@ -172,35 +170,40 @@ Section UPredBI.
   Qed.
 
   (* BI connectives. *)
-  Global Program Instance sc_up : scBI (UPred oRes) :=
+  Global Program Instance sc_up : scBI (UPred Res) :=
     fun P Q =>
-      mkUPred (fun n r => exists r1 r2, r1 · r2 = r /\ P n r1 /\ Q n r2) _.
+      mkUPred (fun n r => exists r1 r2, Some r1 · Some r2 == Some r /\ P n r1 /\ Q n r2) _.
   Next Obligation.
     intros n m r1 r2 HLe [rd HEq] [r11 [r12 [HEq' [HP HQ]]]].
     rewrite <- HEq', assoc in HEq; setoid_rewrite HLe.
+    destruct (Some rd · Some r11) as [r11' |] eqn: HEq'';
+      [| erewrite pcm_op_zero in HEq by apply _; contradiction].
     repeat eexists; [eassumption | | assumption].
-    eapply uni_pred, HP; [| exists rd]; reflexivity.
+    eapply uni_pred, HP; [reflexivity |].
+    exists rd; rewrite HEq''; reflexivity.
   Qed.
 
-  Global Program Instance si_up : siBI (UPred oRes) :=
+  Global Program Instance si_up : siBI (UPred Res) :=
     fun P Q =>
-      mkUPred (fun n r => forall m r' rr, r · r' = rr -> m <= n -> P m r' -> Q m rr) _.
+      mkUPred (fun n r => forall m r' rr, Some r · Some r' == Some rr -> m <= n -> P m r' -> Q m rr) _.
   Next Obligation.
     intros n m r1 r2 HLe [r12 HEq] HSI k r rr HEq' HSub HP.
     rewrite comm in HEq; rewrite <- HEq, <- assoc in HEq'.
-    eapply HSI; [| etransitivity |]; try eassumption; [].
-    eapply uni_pred, HP; [| exists r12]; reflexivity.
+    destruct (Some r12 · Some r) as [r' |] eqn: HEq'';
+      [| erewrite comm, pcm_op_zero in HEq' by apply _; contradiction].
+    eapply HSI; [eassumption | etransitivity; eassumption |].
+    eapply uni_pred, HP; [| exists r12; rewrite HEq'']; reflexivity.
   Qed.
 
   (* Quantifiers. *)
-  Global Program Instance all_up : allBI (UPred oRes) :=
+  Global Program Instance all_up : allBI (UPred Res) :=
     fun T eqT mT cmT R =>
       mkUPred (fun n r => forall t, R t n r) _.
   Next Obligation.
     intros n m r1 r2 HLe HSub HR t; rewrite HLe, <- HSub; apply HR.
   Qed.
 
-  Global Program Instance xist_up : xistBI (UPred oRes) :=
+  Global Program Instance xist_up : xistBI (UPred Res) :=
     fun T eqT mT cmT R =>
       mkUPred (fun n r => exists t, R t n r) _.
   Next Obligation.
@@ -297,23 +300,23 @@ Section UPredBI.
 
     Existing Instance nonexp_type.
 
-    Global Instance all_up_equiv : Proper (equiv (T := V -n> UPred oRes) ==> equiv) all.
+    Global Instance all_up_equiv : Proper (equiv (T := V -n> UPred Res) ==> equiv) all.
     Proof.
       intros R1 R2 EQR n r; simpl.
       setoid_rewrite EQR; tauto.
     Qed.
-    Global Instance all_up_dist n : Proper (dist (T := V -n> UPred oRes) n ==> dist n) all.
+    Global Instance all_up_dist n : Proper (dist (T := V -n> UPred Res) n ==> dist n) all.
     Proof.
       intros R1 R2 EQR m r HLt; simpl.
       split; intros; apply EQR; now auto.
     Qed.
 
-    Global Instance xist_up_equiv : Proper (equiv (T := V -n> UPred oRes) ==> equiv) xist.
+    Global Instance xist_up_equiv : Proper (equiv (T := V -n> UPred Res) ==> equiv) xist.
     Proof.
       intros R1 R2 EQR n r; simpl.
       setoid_rewrite EQR; tauto.
     Qed.
-    Global Instance xist_up_dist n : Proper (dist (T := V -n> UPred oRes)n ==> dist n) xist.
+    Global Instance xist_up_dist n : Proper (dist (T := V -n> UPred Res)n ==> dist n) xist.
     Proof.
       intros R1 R2 EQR m r HLt; simpl.
       split; intros [t HR]; exists t; apply EQR; now auto.
@@ -321,7 +324,7 @@ Section UPredBI.
 
   End Quantifiers.
 
-  Global Program Instance bi_up : ComplBI (UPred oRes).
+  Global Program Instance bi_up : ComplBI (UPred Res).
   Next Obligation.
     intros n r _; exact I.
   Qed.
@@ -357,21 +360,27 @@ Section UPredBI.
     firstorder.
   Qed.
   Next Obligation.
-    intros P Q R n r; simpl; split.
+    intros P Q R n r; split.
     - intros [r1 [rr [EQr [HP [r2 [r3 [EQrr [HQ HR]]]]]]]].
       rewrite <- EQrr, assoc in EQr.
-      exists (r1 · r2) r3; split; [assumption | split; [| assumption] ].
-      exists r1 r2; tauto.
+      destruct (Some r1 · Some r2) as [r12 |] eqn: EQr';
+        [| now erewrite pcm_op_zero in EQr by apply _].
+      exists r12 r3; split; [assumption | split; [| assumption] ].
+      exists r1 r2; split; [rewrite EQr'; reflexivity | split; assumption].
     - intros [rr [r3 [EQr [[r1 [r2 [EQrr [HP HQ]]]] HR]]]].
-      rewrite <- EQrr, <- assoc in EQr.
-      exists r1 (r2 · r3); split; [assumption | split; [assumption |] ].
-      exists r2 r3; tauto.
+      rewrite <- EQrr, <- assoc in EQr; clear EQrr.
+      destruct (Some r2 · Some r3) as [r23 |] eqn: EQ23;
+        [| now erewrite comm, pcm_op_zero in EQr by apply _].
+      exists r1 r23; split; [assumption | split; [assumption |] ].
+      exists r2 r3; split; [rewrite EQ23; reflexivity | split; assumption].
   Qed.
   Next Obligation.
-    intros n r; simpl; split.
+    intros n r; split.
     - intros [r1 [r2 [EQr [_ HP]]]].
       eapply uni_pred, HP; [| exists r1]; trivial.
-    - intros HP; exists 1%pcm r; unfold const; intuition eauto using pcm_op_unit.
+    - intros HP; exists (pcm_unit _) r; split;
+      [erewrite pcm_op_unit by apply _; reflexivity |].
+      simpl; unfold const; tauto.
   Qed.
   Next Obligation.
     split; intros HH n r.
diff --git a/lib/recdom/PCM.v b/lib/recdom/PCM.v
index c1620564fc61e81dd23b4df49d7e9a5f871ad610..e8444d817f879d72efa323300629e0675a46c43b 100644
--- a/lib/recdom/PCM.v
+++ b/lib/recdom/PCM.v
@@ -17,10 +17,10 @@ Section Definitions.
   Class PCM_op   := pcm_op : option T -> option T -> option T.
   Class PCM {TU : PCM_unit} {TOP : PCM_op} :=
     mkPCM {
-        pcm_op_assoc :> Associative (eqT := discreteType) pcm_op;
-        pcm_op_comm  :> Commutative (eqT := discreteType) pcm_op;
-        pcm_op_unit  :  forall t, pcm_op (Some pcm_unit) t = t;
-        pcm_op_zero  :  forall t, pcm_op None t = None
+        pcm_op_assoc  :> Associative pcm_op;
+        pcm_op_comm   :> Commutative pcm_op;
+        pcm_op_unit t : pcm_op (Some pcm_unit) t = t;
+        pcm_op_zero t : pcm_op None t = None
       }.
 
 End Definitions.
@@ -31,11 +31,12 @@ Notation "p · q" := (pcm_op _ p q) (at level 40, left associativity) : pcm_scop
 
 Delimit Scope pcm_scope with pcm.
 
+Instance pcm_eq T `{pcmT : PCM T} : Setoid T | 0 := eqT _.
+
 (* PCMs with cartesian products of carriers. *)
 Section Products.
   Context S T `{pcmS : PCM S, pcmT : PCM T}.
   Local Open Scope pcm_scope.
-  Local Existing Instance eqT.
 
   Global Instance pcm_unit_prod : PCM_unit (S * T) := (pcm_unit S, pcm_unit T).
   Global Instance pcm_op_prod : PCM_op (S * T) :=
@@ -54,29 +55,36 @@ Section Products.
     - intros [[s1 t1] |]; [| reflexivity].
       intros [[s2 t2] |]; [| reflexivity].
       intros [[s3 t3] |];
-        [unfold pcm_op, pcm_op_prod |
-         unfold pcm_op at 1 2, pcm_op_prod;
+        [| unfold pcm_op at 1 2, pcm_op_prod;
            destruct (Some (s1, t1) · Some (s2, t2)) as [[s t] |]; simpl; tauto].
       assert (HS := assoc (Some s1) (Some s2) (Some s3));
         assert (HT := assoc (Some t1) (Some t2) (Some t3)).
+      unfold pcm_op, pcm_op_prod.
       destruct (Some s1 · Some s2) as [s12 |];
         destruct (Some s2 · Some s3) as [s23 |]; [.. | reflexivity].
       + destruct (Some t1 · Some t2) as [t12 |];
         destruct (Some t2 · Some t3) as [t23 |]; [.. | reflexivity].
-        * simpl in HS, HT; rewrite HS, HT; reflexivity.
-        * erewrite comm, pcm_op_zero in HT by eassumption; simpl in HT.
-          rewrite <- HT; destruct (Some s12 · Some s3); reflexivity.
-        * erewrite pcm_op_zero in HT by eassumption; simpl in HT.
-          rewrite HT; destruct (Some s1 · Some s23); reflexivity.
-      + erewrite comm, pcm_op_zero in HS by eassumption; simpl in HS.
+        * destruct (Some s1 · Some s23) as [s |]; destruct (Some s12 · Some s3) as [s' |];
+          try (reflexivity || contradiction); simpl in HS; subst s'; [].
+          destruct (Some t1 · Some t23) as [t |]; destruct (Some t12 · Some t3) as [t' |];
+          try (reflexivity || contradiction); simpl in HT; subst t'; reflexivity.
+        * erewrite comm, pcm_op_zero in HT by apply _.
+          destruct (Some t12 · Some t3); [contradiction |].
+          destruct (Some s12 · Some s3); reflexivity.
+        * erewrite pcm_op_zero in HT by apply _.
+          destruct (Some t1 · Some t23); [contradiction |].
+          destruct (Some s1 · Some s23); reflexivity.
+      + erewrite comm, pcm_op_zero in HS by apply _.
         destruct (Some t1 · Some t2) as [t12 |]; [| reflexivity].
-        rewrite <- HS; reflexivity.
-      + erewrite pcm_op_zero in HS by eassumption; simpl in HS.
+        destruct (Some s12 · Some s3) as [s |]; [contradiction | reflexivity].
+      + erewrite pcm_op_zero in HS by apply _.
         destruct (Some t2 · Some t3) as [t23 |]; [| reflexivity].
-        rewrite HS; reflexivity.
-    - intros [[s1 t1] |] [[s2 t2] |]; try reflexivity; []; simpl; unfold pcm_op, pcm_op_prod.
-      rewrite (comm (Some s1)); assert (HT := comm (Some t1) (Some t2)).
-      simpl in HT; rewrite HT; reflexivity.
+        destruct (Some s1 · Some s23); [contradiction | reflexivity].
+    - intros [[s1 t1] |] [[s2 t2] |]; try reflexivity; []; simpl morph; unfold pcm_op, pcm_op_prod.
+      assert (HS := comm (Some s1) (Some s2)); assert (HT := comm (Some t1) (Some t2)).
+      destruct (Some s1 · Some s2); destruct (Some s2 · Some s1); try (contradiction || exact I); [].
+      destruct (Some t1 · Some t2); destruct (Some t2 · Some t1); try (contradiction || exact I); [].
+      simpl in HS, HT; subst s0 t0; reflexivity.
     - intros [[s t] |]; [| reflexivity]; unfold pcm_op, pcm_op_prod; simpl.
       erewrite !pcm_op_unit by eassumption; reflexivity.
     - intros st; reflexivity.
@@ -87,24 +95,59 @@ End Products.
 Section Order.
   Context T `{pcmT : PCM T}.
   Local Open Scope pcm_scope.
-  Local Existing Instance eqT.
 
-  Definition pcm_ord (t1 t2 : option T) :=
-    exists td, td · t1 = t2.
+  Global Instance pcm_op_equiv : Proper (equiv ==> equiv ==> equiv) (pcm_op _).
+  Proof.
+    intros [s1 |] [s2 |] EQs; try contradiction; [|];
+    [intros [t1 |] [t2 |] EQt; try contradiction; [| rewrite (comm (Some s1)), (comm (Some s2)) ] | intros t1 t2 _];
+    try (erewrite !pcm_op_zero by apply _; reflexivity); [].
+    simpl in EQs, EQt; subst t2 s2; reflexivity.
+  Qed.
+
+  Definition pcm_ord (t1 t2 : T) :=
+    exists td, Some td · Some t1 == Some t2.
+
+  Global Program Instance PCM_preo : preoType T | 0 := mkPOType pcm_ord.
+  Next Obligation.
+    split.
+    - intros x; eexists; erewrite pcm_op_unit by apply _; reflexivity.
+    - intros z yz xyz [y Hyz] [x Hxyz]; unfold pcm_ord.
+      rewrite <- Hyz, assoc in Hxyz; setoid_rewrite <- Hxyz.
+      destruct (Some x · Some y) as [xy |] eqn: Hxy; [eexists; reflexivity |].
+      erewrite pcm_op_zero in Hxyz by apply _; contradiction.
+  Qed.
 
-  Global Program Instance PCM_preo {pcmT : PCM T} : preoType (option T) | 0 := mkPOType pcm_ord.
+  Definition opcm_ord (t1 t2 : option T) :=
+    exists otd, otd · t1 == t2.
+  Global Program Instance opcm_preo : preoType (option T) :=
+    mkPOType opcm_ord.
   Next Obligation.
     split.
-    - intros x; exists 1; eapply pcm_op_unit; assumption.
+    - intros r; exists 1; erewrite pcm_op_unit by apply _; reflexivity.
     - intros z yz xyz [y Hyz] [x Hxyz]; exists (x · y).
-      rewrite <- assoc; congruence.
+      rewrite <- Hxyz, <- Hyz; symmetry; apply assoc.
+  Qed.
+
+  Global Instance equiv_pord_pcm : Proper (equiv ==> equiv ==> equiv) (pord (T := option 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.
+  Qed.
+
+  Global Instance pcm_op_monic : Proper (pord ==> pord ==> pord) (pcm_op _).
+  Proof.
+    intros x1 x2 [x EQx] y1 y2 [y EQy]; exists (x · y).
+    rewrite <- assoc, (comm y), <- assoc, assoc, (comm y1), EQx, EQy; reflexivity.
   Qed.
 
-  Global Instance prod_ord : Proper (pord ==> pord ==> pord) (pcm_op _).
+  Lemma ord_res_optRes r s :
+    (r ⊑ s) <-> (Some r ⊑ Some s).
   Proof.
-    intros x1 x2 [xd EQx] y1 y2 [yd EQy].
-    exists (xd · yd).
-    rewrite <- assoc, (comm yd), <- assoc, assoc, (comm y1); congruence.
+    split; intros HR.
+     - destruct HR as [d EQ]; exists (Some d); assumption.
+     - destruct HR as [[d |] EQ]; [exists d; assumption |].
+       erewrite pcm_op_zero in EQ by apply _; contradiction.
   Qed.
 
 End Order.
diff --git a/world_prop.v b/world_prop.v
index e17c67b3ac2aadb27170f0c3066dd413038e09bf..9e78564400ab020829bf50e49bbc027a910fd01f 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -23,7 +23,7 @@ Module WorldProp (Res : PCM_T).
     Local Instance pcm_disc P `{cmetric P} : pcmType P | 2000 := disc_pcm P.
 
     Definition FProp P `{cmP : cmetric P} :=
-      (nat -f> P) -m> UPred (option res).
+      (nat -f> P) -m> UPred res.
 
     Context {U V} `{cmU : cmetric U} `{cmV : cmetric V}.