diff --git a/iris_derived_rules.v b/iris_derived_rules.v
index 3d4b04cb8e1c18277f63989d811460bb2931940a..eb9452559fb19f20427c36f6db7f341bf0114bb6 100644
--- a/iris_derived_rules.v
+++ b/iris_derived_rules.v
@@ -15,8 +15,6 @@ Module Type IRIS_DERIVED_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (W
 
   Section DerivedRules.
 
-    Existing Instance LP_isval.
-
     Implicit Types (P : Props) (i : nat) (m : mask) (e : expr) (r : res).
 
     Lemma vsFalse m1 m2 :
diff --git a/iris_ht_rules.v b/iris_ht_rules.v
index 7d5f1e5f4b00a2571d8a8488c91d03986bac923a..203e9d70c28962e72e3c60e4bdbd0bb38d93a131 100644
--- a/iris_ht_rules.v
+++ b/iris_ht_rules.v
@@ -16,7 +16,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
 
     Existing Instance LP_isval.
 
-    Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : pres).
+    Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : res).
 
     (** Ret **)
     Program Definition eqV v : vPred :=
@@ -247,24 +247,20 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       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. exists w''.
-        exists↓ (ra_proj r1' · ra_proj r2).
-        { apply wsat_valid in HE. auto_valid. }
+        rewrite ->assoc in HE. exists w'' (r1' · r2).
         split; [eassumption | split; [| eassumption ] ].
         exists r1' r2; split; [reflexivity | 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. exists w''. exists↓ (ra_proj r1' · ra_proj r2).
-        { apply wsat_valid in HE. auto_valid. }
+        rewrite ->assoc in HE. exists w'' (r1' · r2).
         split; [eassumption | split; [| eassumption] ].
         eapply IH; try eassumption; [ reflexivity |].
         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 (_ rfk)) in HE.
-        exists w''. exists rfk. exists↓ (ra_proj rret · ra_proj r2).
-        { clear- HE. apply wsat_valid in HE. eapply ra_op_valid2, ra_op_valid; try now apply _. eassumption. }
+        rewrite ->assoc, <- (assoc rfk) in HE.
+        exists w''. exists rfk (rret · r2).
         split; [eassumption | split; [| split; eassumption] ].
         eapply IH; try eassumption; [ reflexivity |].
         unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
@@ -288,8 +284,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         edestruct He as [_ [HeS _] ]; try eassumption; [].
         edestruct HeS as [w'' [r1' [HSw' [He' HE'] ] ] ]; try eassumption; [].
         clear HE He HeS; rewrite ->assoc in HE'.
-        exists w''. exists↓ (ra_proj r1' · ra_proj r2).
-        { clear- HE'. apply wsat_valid in HE'. auto_valid. }
+        exists w'' (r1' · r2).
         split; [eassumption | split; [| eassumption] ].
         assert (HNV : ~ is_value ei)
           by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
@@ -299,12 +294,11 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         assert (HVal := atomic_step _ _ _ _ HAt HStep).
         clear - He' HVal 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 ra_proj_cancel in HE. rewrite <-assoc in HE.
+        + rewrite ->unfold_wp in He'. rewrite <-assoc in HE.
           edestruct He' as [HVal _]; try eassumption; [].
           specialize (HVal HV); destruct HVal as [w'' [r1'' [HSw' [Hφ HE'] ] ] ].
           rewrite ->assoc in HE'.
-          exists w''. exists↓ (ra_proj r1'' · ra_proj r2).
-          { clear- HE'. apply wsat_valid in HE'. auto_valid. }
+          exists w'' (r1'' · r2).
           split; [eassumption | split; [| eassumption] ].
           exists r1'' r2; split; [reflexivity | split; [assumption |] ].
           unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; apply HLR.
@@ -315,7 +309,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         + unfold safeExpr. now auto.
       - subst; eapply fork_not_atomic; eassumption.
       - rewrite <- EQr, <- assoc in HE; rewrite ->unfold_wp in He.
-        specialize (He w' k (ra_proj r2 · rf) mf σ HSw HLt HD0 HE); clear HE.
+        specialize (He w' k (r2 · rf) mf σ HSw HLt HD0 HE); clear HE.
         destruct He as [_ [_ [_ HS'] ] ]; auto.
     Qed.
 
@@ -339,7 +333,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         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 (ra_pos_unit) r2; split; [unfold ra_pos_unit; simpl; now erewrite ra_op_unit by apply _ |].
+          exists 1 r2; split; [simpl; now erewrite ra_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].
diff --git a/iris_vs_rules.v b/iris_vs_rules.v
index 5b905802b583ae68295efbeed8b366afe33df548..31b32531f20e507ef2a0a5e4f823ecee8c0451b6 100644
--- a/iris_vs_rules.v
+++ b/iris_vs_rules.v
@@ -11,7 +11,7 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
   Local Open Scope bi_scope.
   Local Open Scope iris_scope.
 
-  Implicit Types (P Q R : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (σ : state).
+  Implicit Types (P Q R : Props) (w : Wld) (n i k : nat) (m : mask) (r : res) (σ : state).
 
   Section ViewShiftProps.
 
@@ -38,14 +38,13 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       destruct HE as [rs [HE HM] ].
       destruct (rs i) as [ri |] eqn: HLr.
       - rewrite ->comp_map_remove with (i := i) (r := ri) in HE by now eapply equivR.
-        rewrite ->assoc, <- (assoc (_ r)), (comm rf), assoc in HE.
-        exists w'.
-        exists↓ (ra_proj r · ra_proj ri). { destruct HE as [HE _]. eapply ra_op_valid, ra_op_valid; eauto with typeclass_instances. }
+        rewrite ->assoc, <- (assoc r), (comm rf), assoc in HE.
+        exists w' (r · ri).
         split; [reflexivity |].
         split.
         + simpl; eapply HInv; [now auto with arith |].
           eapply uni_pred, HM with i;
-            [| exists (ra_proj r) | | | rewrite HLr]; try reflexivity; [reflexivity| |].
+            [| exists r | | | rewrite HLr]; try reflexivity.
           * left; unfold mask_sing, mask_set.
             destruct (Peano_dec.eq_nat_dec i i); tauto.
           * specialize (HSub i); rewrite HLu in HSub.
@@ -72,17 +71,10 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       (* get rid of the invisible 1/2 *)
       do 8 red in HInv.
       destruct HE as [rs [HE HM] ].
-      exists w' ra_pos_unit; split; [reflexivity | split; [exact I |] ].
-      rewrite ->(comm (_ r)), <-assoc in HE.
-      remember (match rs i with Some ri => ri | None => ra_pos_unit end) as ri eqn: EQri.
-      pose↓ rri := (ra_proj ri · ra_proj r).
-      { destruct (rs i) as [rsi |] eqn: EQrsi; subst;
-        [| simpl; rewrite ->ra_op_unit by apply _; now apply ra_pos_valid].
-        clear - HE EQrsi. destruct HE as [HE _].
-        rewrite ->comp_map_remove with (i:=i) in HE by (eapply equivR; eassumption).
-        rewrite ->(assoc (_ r)), (comm (_ r)), comm, assoc, <-(assoc (_ rsi) _), (comm _ (ra_proj r)), assoc in HE.
-        eapply ra_op_valid, ra_op_valid; now eauto with typeclass_instances.
-      }
+      exists w' 1; split; [reflexivity | split; [exact I |] ].
+      rewrite ->(comm r), <-assoc in HE.
+      remember (match rs i with Some ri => ri | None => 1 end) as ri eqn: EQri.
+      pose (rri := (ri · r)).
       exists (fdUpdate i rri rs); split; [| intros j Hm].
       - simpl. erewrite ra_op_unit by apply _.
         clear - HE EQri. destruct (rs i) as [rsi |] eqn: EQrsi.
@@ -102,11 +94,8 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         apply HInv; [now auto with arith |].
         eapply uni_pred, HP; [now auto with arith |].
         rewrite <-HLrs. clear dependent ri0.
-        exists (ra_proj ri · ra_proj r1).
-        subst rri.
-        (* Coq, are you serious?!?? *)
-        change (ra_proj ri · ra_proj r1 · ra_proj r2 == (ra_proj ri · ra_proj r)).
-        rewrite <-HR, assoc. reflexivity.
+        exists (ri · r1).
+        subst rri. rewrite <-HR, assoc. reflexivity.
     Qed.
 
     Lemma vsTrans P Q R m1 m2 m3 (HMS : m2 ⊆ m1 ∪ m3) :
@@ -134,7 +123,7 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       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; split; [reflexivity | split; [| assumption ] ].
-      eapply Himp; [assumption | now eauto with arith | now apply ord_res_pres, unit_min | ].
+      eapply Himp; [assumption | now eauto with arith | now apply unit_min | ].
       unfold lt in HLe0; rewrite ->HLe0, <- HSub; assumption.
     Qed.
 
@@ -143,8 +132,8 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
     Proof.
       intros w' n r1 HVS w HSub; specialize (HVS _ HSub); clear w' r1 HSub.
       intros np rpr HLe _ [rp [rr [HR [Hp Hr] ] ] ] w'; intros.
-      assert (HS : ra_unit _ ⊑ ra_proj rp) by (eapply unit_min).
-      specialize (HVS _ _ HLe HS Hp w' (ra_proj rr · rf) (mf ∪ mf0) σ k); clear HS.
+      assert (HS : ra_unit _ ⊑ rp) by (eapply unit_min).
+      specialize (HVS _ _ HLe HS Hp w' (rr · rf) (mf ∪ mf0) σ k); clear HS.
       destruct HVS as [w'' [rq [HSub' [Hq HEq] ] ] ]; try assumption; [| |].
       - (* disjointness of masks: possible lemma *)
         clear - HD HDisj; intros i [ [Hmf | Hmf] Hm12]; [eapply HDisj; now eauto |].
@@ -152,8 +141,7 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       - rewrite ->assoc, HR; eapply wsat_equiv, HE; try reflexivity; [].
         clear; intros i; unfold mcup; tauto.
       - rewrite ->assoc in HEq.
-        exists w''. exists↓ (ra_proj rq · ra_proj rr).
-        { apply wsat_valid in HEq. auto_valid. }
+        exists w'' (rq · rr).
         split; [assumption | split].
         + unfold lt in HLe0; rewrite ->HSub, HSub', <- HLe0 in Hr; exists rq rr.
           split; now auto.
@@ -174,18 +162,14 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
           (HU : forall rf (HD : ↓(rl · rf)), exists sl, P sl /\ ↓(sl · rf)) :
       valid (vs m m (ownL rl) (xist (ownLP P))).
     Proof.
-      unfold ownLP; intros _ _ _ w _ n [ [rp' rl'] Hrval] _ _ HG w'; intros.
-      destruct HE as [rs [ Hsat HE] ]. rewrite <-assoc in Hsat. simpl in Hsat. destruct Hsat as [Hval Hst].
+      unfold ownLP; intros _ _ _ w _ n [rp' rl'] _ _ HG w'; intros.
+      destruct HE as [rs [ Hsat HE] ]. rewrite <-assoc in Hsat. destruct Hsat as [Hval Hst].
       destruct HG as [ [rdp rdl] [_ EQrl] ]. simpl in EQrl. clear rdp.
       destruct (HU (rdl · snd(rf · comp_map rs))) as [rsl [HPrsl HCrsl] ].
       - clear - Hval EQrl. eapply ra_prod_valid in Hval. destruct Hval as [_ Hsnd].
         rewrite ->assoc, (comm rl), EQrl.
         rewrite ra_op_prod_snd in Hsnd. exact Hsnd.
-      - exists w'. exists↓ (rp', rsl).
-        { clear - Hval HCrsl.
-          apply ra_prod_valid. split; [|auto_valid].
-          eapply ra_prod_valid in Hval. destruct Hval as [Hfst _].
-          rewrite ra_op_prod_fst in Hfst. auto_valid. }
+      - exists w' (rp', rsl).
         split; first reflexivity. split.
         + exists (exist _ rsl HPrsl). simpl.
           exists (rp', 1:RL.res). simpl.
@@ -239,10 +223,10 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       { intros j; destruct (Peano_dec.eq_nat_dec i j); [subst j; rewrite HLi; exact I|].
         now rewrite ->fdUpdate_neq by assumption.
       }
-      exists (fdUpdate i (ı' P) w) (ra_pos_unit); split; [assumption | split].
+      exists (fdUpdate i (ı' P) w) 1; split; [assumption | split].
       - exists (exist _ i Hm). do 22 red.
         unfold proj1_sig. rewrite fdUpdate_eq; reflexivity.
-      - unfold ra_pos_unit, proj1_sig. erewrite ra_op_unit by apply _.
+      - erewrite ra_op_unit by apply _.
         destruct HE as [rs [HE HM] ].
         exists (fdUpdate i r rs).
         assert (HRi : rs i = None).
@@ -264,6 +248,18 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
           apply HM; assumption.
     Qed.
 
+    Lemma vsNotOwnInvalid m1 m2 r
+      (Hnval: ~↓r):
+      valid (vs m1 m2 (ownR r) ⊥).
+    Proof.
+      intros pw n s w _. clear pw s.
+      intros m s _ _. clear n.
+      intros [rs Heq] w' rf mf σ k _ _ _ [ ri [ [ Hval _ ] ] ].
+      exfalso.
+      apply Hnval. rewrite <-Heq in Hval.
+      eapply ra_op_valid2, ra_op_valid, ra_op_valid; last eassumption; now apply _.
+    Qed.
+
   End ViewShiftProps.
 
 End IRIS_VS_RULES.