diff --git a/theories/examples/or.v b/theories/examples/or.v
index f09352a816e919bbd8a146b424d320e79a528c5d..00ed7125c417c8931d67ce380222195bbeb6b968 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -153,7 +153,7 @@ Section rules.
   Qed.
 
   (** Associativity *)
-  Lemma or_assoc_l e1 e2 e3 e1' e2' e3' A :
+  Lemma or_assoc_l_v e1 e2 e3 e1' e2' e3' A :
     (REL e1 << e1' : A) -∗
     (REL e2 << e2' : A) -∗
     (REL e3 << e3' : A) -∗
@@ -168,16 +168,48 @@ Section rules.
     - rel_apply_r or_refines_r. by iRight.
   Qed.
 
+  Lemma or_assoc_l e1 e2 e3 e1' e2' e3' A :
+    (REL e1 << e1' : A) -∗
+    (REL e2 << e2' : A) -∗
+    (REL e3 << e3' : A) -∗
+    REL (e1 ⊕ (e2 ⊕ e3)) << ((e1' ⊕ e2') ⊕ e3') : A.
+  Proof.
+    iIntros "H1 H2 H3".
+    rel_pures_r.
+    repeat (rel_pures_l; rel_apply_l or_refines_l; iSplit).
+    - rel_apply_r or_refines_r. iLeft.
+      rel_pures_r. rel_apply_r or_refines_r. by iLeft.
+    - rel_apply_r or_refines_r. iLeft.
+      rel_pures_r. rel_apply_r or_refines_r. by iRight.
+    - rel_apply_r or_refines_r. by iRight.
+  Qed.
+
+  Lemma or_assoc_r e1 e2 e3 e1' e2' e3' A :
+    (REL e1 << e1' : A) -∗
+    (REL e2 << e2' : A) -∗
+    (REL e3 << e3' : A) -∗
+    REL ((e1 ⊕ e2) ⊕ e3) << (e1' ⊕ (e2' ⊕ e3')) : A.
+  Proof.
+    iIntros "H1 H2 H3".
+    rel_pures_r.
+    repeat (rel_pures_l; rel_apply_l or_refines_l; iSplit).
+    - rel_apply_r or_refines_r. by iLeft.
+    - rel_apply_r or_refines_r. iRight.
+      rel_pures_r. rel_apply_r or_refines_r. by iLeft.
+    - rel_apply_r or_refines_r. iRight.
+      rel_pures_r. rel_apply_r or_refines_r. by iRight.
+  Qed.
+
   (** Interaction between OR and sequencing. *)
   (** Standard in algebraic models of programming. *)
   Lemma or_seq_1 (f g h f' g' h' : expr) A :
     (REL f << f' : A) -∗
     (REL g << g' : A) -∗
     (REL h << h' : A) -∗
-    REL ((f ⊕ g)%V;; h)
-      << ((f';; h') ⊕ (g';; h'))%V : A.
+    REL ((f ⊕ g);; h)
+      << ((f';; h') ⊕ (g';; h')) : A.
   Proof.
-    iIntros "Hf Hg Hh".
+    iIntros "Hf Hg Hh". rel_pures_l. rel_pures_r.
     rel_apply_l or_refines_l; iSplit; simpl.
     - rel_apply_r or_refines_r.
       iLeft. iApply (refines_seq with "Hf Hh").
@@ -188,10 +220,10 @@ Section rules.
     (REL f << f' : A) -∗
     (REL g << g' : A) -∗
     (REL h << h' : A) -∗
-    REL ((f;; h) ⊕ (g;; h))%V
-      << ((f' ⊕ g')%V;; h') : A.
+    REL ((f;; h) ⊕ (g;; h))
+      << ((f' ⊕ g');; h') : A.
   Proof.
-    iIntros "Hf Hg Hh".
+    iIntros "Hf Hg Hh". rel_pures_l. rel_pures_r.
     rel_apply_l or_refines_l; iSplit; simpl.
     - rel_apply_r or_refines_r.
       iLeft. iApply (refines_seq with "Hf Hh").
@@ -206,15 +238,15 @@ Section rules.
     (REL f << f' : A) -∗
     (REL g << g' : A) -∗
     (REL h << h' : A) -∗
-    REL ((f;; g) ⊕ (f;; h))%V
-      << (f';; (g' ⊕ h')%V) : A.
+    REL ((f;; g) ⊕ (f;; h))
+      << (f';; (g' ⊕ h')) : A.
   Proof.
-    iIntros "Hf Hg Hh".
+    iIntros "Hf Hg Hh". rel_pures_l.
     rel_apply_l or_refines_l. iSplit.
     - iApply (refines_seq with "Hf").
-      rel_apply_r or_refines_r. by iLeft.
+      rel_pures_r. rel_apply_r or_refines_r. by iLeft.
     - iApply (refines_seq with "Hf").
-      rel_apply_r or_refines_r. by iRight.
+      rel_pures_r. rel_apply_r or_refines_r. by iRight.
   Qed.
 
 
@@ -238,9 +270,9 @@ Section rules.
          f;;
          (((resolve_proph: "p" to: #0);; g) ⊕
           ((resolve_proph: "p" to: #1);; h))%E) << (* Here we *have to* use the expr scope, otherwise "p" won't be substituted *)
-      ((f';; g') ⊕ (f';; h'))%V : A.
+      ((f';; g') ⊕ (f';; h')) : A.
   Proof.
-    iIntros (???) "Hf Hg Hh".
+    iIntros (???) "Hf Hg Hh". rel_pures_r.
     rel_newproph_l vs p as "Hp". repeat rel_pure_l.
     (rewrite !(subst_is_closed []) //; try by set_solver); [].
     rel_apply_r or_refines_r.
@@ -271,7 +303,7 @@ Section rules.
     (REL f << f' : A) -∗
     (REL g << g' : A) -∗
     (REL h << h' : A) -∗
-    REL (f;; (g ⊕ h)%V) <<
+    REL (f;; (g ⊕ h)) <<
     (let: "p" := NewProph in
          f';;
          (((resolve_proph: "p" to: #0);; g') ⊕
@@ -281,7 +313,8 @@ Section rules.
     rel_newproph_r p. repeat rel_pure_r.
     (rewrite !(subst_is_closed []) //; try by set_solver); [].
     iApply (refines_seq with "Hf").
-    repeat rel_pure_r. iApply (or_compatible with "[Hg] [Hh]").
+    rel_pures_l. rel_pures_r.
+    iApply (or_compatible with "[Hg] [Hh]").
     - rel_resolveproph_r. by repeat rel_pure_r.
     - rel_resolveproph_r. by repeat rel_pure_r.
   Qed.
diff --git a/theories/examples/par.v b/theories/examples/par.v
index 666cc2e5d67ef2875088a9d1a138060cf51dbb05..422a87cc1b40f679b3c60f84e75cc4108e4f022c 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -45,43 +45,42 @@ Section rules.
   (* this one we can prove without unfolding *)
   Lemma par_unit_1 e A :
     (REL e << e : A) -∗
-    REL (#() ||| e)%V << e : lrel_true.
+    REL (#() ||| e) << e : lrel_true.
   Proof.
     iIntros "He".
-    rel_rec_l. repeat rel_pure_l.
+    rel_pures_l. rel_rec_l. rel_pures_l.
     rel_bind_l (spawn _).
     iApply refines_wp_l.
     pose (N:=nroot.@"par").
     iApply (spawn_spec N (λ v, True)%I).
     - by wp_pures.
     - iNext. iIntros (l) "hndl". iSimpl.
-      repeat rel_pure_l. rel_bind_l e. rel_bind_r e.
+      rel_pures_l. rel_bind_l e. rel_bind_r e.
       iApply (refines_bind with "He").
       iIntros (v v') "Hv". simpl.
-      repeat rel_pure_l.
+      rel_pures_l.
       rel_bind_l (spawn.join _).
       iApply refines_wp_l.
       iApply (join_spec with "hndl").
       iNext. iIntros (?) "_". simpl.
-      repeat rel_pure_l. rel_values.
+      rel_pures_l. rel_values.
   Qed.
   Lemma par_unit_2 e A :
     (REL e << e : A) -∗
-    REL e << (#() ||| e)%V : lrel_true.
+    REL e << (#() ||| e) : lrel_true.
   Proof.
     iIntros "H".
-    rel_rec_r. repeat rel_pure_r.
-    rel_rec_r.
-    repeat rel_pure_r. rel_alloc_r c2 as "Hc2".
-    repeat rel_pure_r. rel_fork_r i as "Hi".
-    repeat rel_pure_r.
+    rel_pures_r. rel_rec_r. rel_pures_r. rel_rec_r.
+    rel_pures_r. rel_alloc_r c2 as "Hc2".
+    rel_pures_r. rel_fork_r i as "Hi".
+    rel_pures_r.
     tp_rec i. simpl.
     tp_pure i _. tp_store i.
     rel_bind_l e. rel_bind_r e.
     iApply (refines_bind with "H").
     iIntros (v v') "Hv". simpl.
-    repeat rel_pure_r.
-    rel_rec_r. rel_load_r. repeat rel_pure_r.
+    rel_pures_r.
+    rel_rec_r. rel_load_r. rel_pures_r.
     rel_values.
   Qed.