diff --git a/algebra/upred.v b/algebra/upred.v
index c44d093186b32c3caa509646b7822fc0b6f26cc1..2a974d2be07004f07f8a60ca36320dff72fb9881 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -300,8 +300,16 @@ Infix "≡" := uPred_eq : uPred_scope.
 Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
 
 Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
+Instance: Params (@uPred_iff) 1.
 Infix "↔" := uPred_iff : uPred_scope.
 
+Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
+  (if p then â–¡ P else P)%I.
+Instance: Params (@uPred_always_if) 2.
+Arguments uPred_always_if _ !_ _/.
+Notation "â–¡? p P" := (uPred_always_if p P)
+  (at level 20, p at level 0, P at level 20, format "â–¡? p  P").
+
 Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ (P ∨ ▷ False).
 Arguments timelessP {_} _ {_}.
 
@@ -935,6 +943,28 @@ Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
 Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ (P ★ □ Q).
 Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
 
+Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
+Proof. solve_proper. Qed.
+Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
+Proof. solve_proper. Qed.
+Global Instance always_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M p).
+Proof. solve_proper. Qed.
+
+Lemma always_if_elim p P : □?p P ⊢ P.
+Proof. destruct p; simpl; auto using always_elim. Qed.
+Lemma always_elim_if p P : □ P ⊢ □?p P.
+Proof. destruct p; simpl; auto using always_elim. Qed.
+Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ (□?p P ∧ □?p Q).
+Proof. destruct p; simpl; auto using always_and. Qed.
+Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ (□?p P ∨ □?p Q).
+Proof. destruct p; simpl; auto using always_or. Qed.
+Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ (∃ a, □?p Ψ a).
+Proof. destruct p; simpl; auto using always_exist. Qed.
+Lemma always_if_sep p P Q : □?p (P ★ Q) ⊣⊢ (□?p P ★ □?p Q).
+Proof. destruct p; simpl; auto using always_sep. Qed.
+Lemma always_if_later p P : (□?p ▷ P) ⊣⊢ (▷ □?p P).
+Proof. destruct p; simpl; auto using always_later. Qed.
+
 (* Later *)
 Lemma later_mono P Q : P ⊢ Q → ▷ P ⊢ ▷ Q.
 Proof.
@@ -1117,6 +1147,8 @@ Proof.
   intros ?; rewrite /TimelessP.
   by rewrite -always_const -!always_later -always_or; apply always_mono.
 Qed.
+Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?p P).
+Proof. destruct p; apply _. Qed.
 Global Instance eq_timeless {A : cofeT} (a b : A) :
   Timeless a → TimelessP (a ≡ b : uPred M)%I.
 Proof.
@@ -1165,6 +1197,8 @@ Proof. destruct mx; apply _. Qed.
 (* Derived lemmas for persistence *)
 Lemma always_always P `{!PersistentP P} : (□ P) ⊣⊢ P.
 Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
+Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P.
+Proof. destruct p; simpl; auto using always_always. Qed.
 Lemma always_intro P Q `{!PersistentP P} : P ⊢ Q → P ⊢ □ Q.
 Proof. rewrite -(always_always P); apply always_intro'. Qed.
 Lemma always_and_sep_l P Q `{!PersistentP P} : (P ∧ Q) ⊣⊢ (P ★ Q).
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 17a8778f9650d440b73c7453f224fcd48aaf0586..4bf9450852b1e88c18359f15dc0a24ba40e490b2 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -77,8 +77,8 @@ Definition envs_replace {M} (i : string) (p q : bool) (Γ : env (uPred M))
   if eqb p q then envs_simple_replace i p Γ Δ
   else envs_app q Γ (envs_delete i p Δ).
 
-(* if [lr = false] then [result = (hyps named js,remainding hyps)],
-   if [lr = true] then [result = (remainding hyps,hyps named js)] *)
+(* if [lr = false] then [result = (hyps named js, remaining hyps)],
+   if [lr = true] then [result = (remaining hyps, hyps named js)] *)
 Definition envs_split {M}
     (lr : bool) (js : list string) (Δ : envs M) : option (envs M * envs M) :=
   let (Γp,Γs) := Δ in
@@ -115,8 +115,7 @@ Proof.
 Qed.
 
 Lemma envs_lookup_sound Δ i p P :
-  envs_lookup i Δ = Some (p,P) →
-  Δ ⊢ ((if p then □ P else P) ★ envs_delete i p Δ).
+  envs_lookup i Δ = Some (p,P) → Δ ⊢ (□?p P ★ envs_delete i p Δ).
 Proof.
   rewrite /envs_lookup /envs_delete /of_envs=>?; apply const_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -132,9 +131,7 @@ Proof.
 Qed.
 Lemma envs_lookup_sound' Δ i p P :
   envs_lookup i Δ = Some (p,P) → Δ ⊢ (P ★ envs_delete i p Δ).
-Proof.
-  intros. rewrite envs_lookup_sound //. by destruct p; rewrite ?always_elim.
-Qed.
+Proof. intros. rewrite envs_lookup_sound //. by rewrite always_if_elim. Qed.
 Lemma envs_lookup_persistent_sound Δ i P :
   envs_lookup i Δ = Some (true,P) → Δ ⊢ (□ P ★ Δ).
 Proof.
@@ -142,8 +139,7 @@ Proof.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
-  envs_lookup i Δ = Some (p,P) →
-  Δ ⊢ ((if p then □ P else P) ★ ((if p then □ P else P) -★ Δ)).
+  envs_lookup i Δ = Some (p,P) → Δ ⊢ (□?p P ★ (□?p P -★ Δ)).
 Proof.
   rewrite /envs_lookup /of_envs=>?; apply const_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -156,14 +152,13 @@ Proof.
 Qed.
 
 Lemma envs_lookup_delete_sound Δ Δ' i p P :
-  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ ((if p then □ P else P) ★ Δ')%I.
+  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ (□?p P ★ Δ')%I.
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
 Lemma envs_lookup_delete_sound' Δ Δ' i p P :
   envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ (P ★ Δ')%I.
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
 
-Lemma envs_app_sound Δ Δ' p Γ :
-  envs_app p Γ Δ = Some Δ' → Δ ⊢ ((if p then □ Π∧ Γ else Π★ Γ) -★ Δ').
+Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' → Δ ⊢ (□?p Π★ Γ -★ Δ').
 Proof.
   rewrite /of_envs /envs_app=> ?; apply const_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -174,7 +169,8 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
     + rewrite (env_app_perm _ _ Γp') //.
-      rewrite big_and_app always_and_sep always_sep; solve_sep_entails.
+      rewrite big_and_app always_and_sep always_sep (big_sep_and Γ).
+      solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
@@ -186,7 +182,7 @@ Qed.
 
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
   envs_simple_replace i p Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ ((if p then □ Π∧ Γ else Π★ Γ) -★ Δ')%I.
+  envs_delete i p Δ ⊢ (□?p Π★ Γ -★ Δ')%I.
 Proof.
   rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
   apply const_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -197,7 +193,8 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
     + rewrite (env_replace_perm _ _ Γp') //.
-      rewrite big_and_app always_and_sep always_sep; solve_sep_entails.
+      rewrite big_and_app always_and_sep always_sep (big_sep_and Γ).
+      solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
@@ -209,13 +206,11 @@ Qed.
 
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  Δ ⊢ ((if p then □ P else P) ★
-       ((if p then □ Π∧ Γ else Π★ Γ) -★ Δ'))%I.
+  Δ ⊢ (□?p P ★ (□?p Π★ Γ -★ Δ'))%I.
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
 Lemma envs_replace_sound' Δ Δ' i p q Γ :
-  envs_replace i p q Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ ((if q then □ Π∧ Γ else Π★ Γ) -★ Δ')%I.
+  envs_replace i p q Γ Δ = Some Δ' → envs_delete i p Δ ⊢ (□?q Π★ Γ -★ Δ')%I.
 Proof.
   rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
@@ -224,8 +219,7 @@ Qed.
 
 Lemma envs_replace_sound Δ Δ' i p q P Γ :
   envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
-  Δ ⊢ ((if p then □ P else P) ★
-       ((if q then □ Π∧ Γ else Π★ Γ) -★ Δ'))%I.
+  Δ ⊢ (□?p P ★ (□?q Π★ Γ -★ Δ'))%I.
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
 
 Lemma envs_split_sound Δ lr js Δ1 Δ2 :
@@ -299,10 +293,9 @@ Proof.
 Qed.
 
 (** * Basic rules *)
-Class ToAssumption (p : bool) (P Q : uPred M) :=
-  to_assumption : (if p then □ P else P) ⊢ Q.
+Class ToAssumption (p : bool) (P Q : uPred M) := to_assumption : □?p P ⊢ Q.
 Global Instance to_assumption_exact p P : ToAssumption p P P.
-Proof. destruct p; by rewrite /ToAssumption ?always_elim. Qed.
+Proof. destruct p; by rewrite /ToAssumption /= ?always_elim. Qed.
 Global Instance to_assumption_always P Q :
   ToAssumption true P Q → ToAssumption true P (□ Q).
 Proof. rewrite /ToAssumption=><-. by rewrite always_always. Qed.
@@ -418,9 +411,8 @@ Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
   Δ' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros ??? <-. rewrite envs_replace_sound //; simpl. destruct p.
-  - by rewrite right_id (to_persistentP P) always_always wand_elim_r.
-  - by rewrite right_id (to_persistentP P) wand_elim_r.
+  intros ??? <-. rewrite envs_replace_sound //; simpl.
+  by rewrite right_id (to_persistentP P) always_if_always wand_elim_r.
 Qed.
 
 (** * Implication and wand *)
@@ -448,8 +440,7 @@ Qed.
 Lemma tac_wand_intro Δ Δ' i P Q :
   envs_app false (Esnoc Enil i P) Δ = Some Δ' → Δ' ⊢ Q → Δ ⊢ (P -★ Q).
 Proof.
-  intros. rewrite envs_app_sound //; simpl.
-  rewrite right_id. by apply wand_mono.
+  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
 Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
   ToPersistentP P P' →
@@ -490,14 +481,11 @@ Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
 Proof.
   intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
   - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
-    destruct q.
-    + by rewrite assoc (to_wand R) always_wand wand_elim_r right_id wand_elim_r.
-    + by rewrite assoc (to_wand R) always_elim wand_elim_r right_id wand_elim_r.
+    rewrite assoc (to_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
+    by rewrite right_id wand_elim_r.
   - rewrite envs_lookup_sound //; simpl.
     rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
-    destruct q.
-    + by rewrite right_id assoc (to_wand R) always_elim wand_elim_r wand_elim_r.
-    + by rewrite assoc (to_wand R) wand_elim_r right_id wand_elim_r.
+    by rewrite right_id assoc (to_wand R) always_if_elim wand_elim_r wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js P1 P2 R Q :
@@ -513,12 +501,11 @@ Proof.
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_sound Δ2) //; simpl.
-  destruct q, (envs_persistent Δ1) eqn:?; simplify_eq/=.
+  destruct (envs_persistent Δ1) eqn:?; simplify_eq/=.
   - rewrite right_id (to_wand R) (persistentP Δ1) HP1.
-    by rewrite assoc -always_sep wand_elim_l wand_elim_r.
-  - by rewrite right_id (to_wand R) always_elim assoc HP1 wand_elim_l wand_elim_r.
-  - by rewrite right_id (to_wand R) assoc HP1 wand_elim_l wand_elim_r.
-  - by rewrite right_id (to_wand R) assoc HP1 wand_elim_l wand_elim_r. 
+    by rewrite assoc (always_elim_if q) -always_if_sep wand_elim_l wand_elim_r.
+  - rewrite right_id (to_wand R).
+    by rewrite always_if_elim assoc HP1 wand_elim_l wand_elim_r.
 Qed.
 
 Lemma tac_specialize_range_persistent Δ Δ' Δ'' j q P1 P2 R Q :
@@ -531,9 +518,9 @@ Proof.
   rewrite envs_lookup_sound //.
   rewrite -(idemp uPred_and (envs_delete _ _ _)).
   rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
-  rewrite envs_simple_replace_sound' //; simpl. destruct q.
-  - by rewrite right_id (to_wand R) -always_sep wand_elim_l wand_elim_r.
-  - by rewrite right_id (to_wand R) always_elim wand_elim_l wand_elim_r.
+  rewrite envs_simple_replace_sound' //; simpl.
+  rewrite right_id (to_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
+  by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_specialize_domain_persistent Δ Δ' Δ'' j q P1 P2 P2' R Q :
@@ -545,11 +532,8 @@ Proof.
   intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
   rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
   rewrite envs_replace_sound //; simpl.
-  rewrite (sep_elim_r _ (_ -★ _)) right_id. destruct q.
-  - rewrite (to_wand R) always_elim wand_elim_l.
-    by rewrite (to_persistentP P2) always_and_sep_l' wand_elim_r.
-  - rewrite (to_wand R) wand_elim_l.
-    by rewrite (to_persistentP P2) always_and_sep_l' wand_elim_r.
+  rewrite (sep_elim_r _ (_ -★ _)) right_id (to_wand R) always_if_elim.
+  by rewrite wand_elim_l (to_persistentP P2) always_and_sep_l' wand_elim_r.
 Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
@@ -655,15 +639,11 @@ Proof.
   intros ?? A Δ' x y Φ HPxy HP ?? <-.
   rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
   rewrite sep_elim_l HPxy always_and_sep_r.
-  rewrite (envs_simple_replace_sound _ _ j) //; simpl. destruct q.
-  - rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
-    + apply (eq_rewrite x y (λ y, □ Φ y -★ Δ')%I); eauto with I. solve_proper.
-    + apply (eq_rewrite y x (λ y, □ Φ y -★ Δ')%I); eauto using eq_sym with I.
-      solve_proper.
-  - rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
-    + apply (eq_rewrite x y (λ y, Φ y -★ Δ')%I); eauto with I. solve_proper.
-    + apply (eq_rewrite y x (λ y, Φ y -★ Δ')%I); eauto using eq_sym with I.
-      solve_proper.
+  rewrite (envs_simple_replace_sound _ _ j) //; simpl.
+  rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
+  - apply (eq_rewrite x y (λ y, □?q Φ y -★ Δ')%I); eauto with I. solve_proper.
+  - apply (eq_rewrite y x (λ y, □?q Φ y -★ Δ')%I); eauto using eq_sym with I.
+    solve_proper.
 Qed.
 
 (** * Conjunction splitting *)
@@ -725,10 +705,10 @@ Qed.
 
 (** * Conjunction/separating conjunction elimination *)
 Class SepDestruct (p : bool) (P Q1 Q2 : uPred M) :=
-  sep_destruct : if p then □ P ⊢ □ (Q1 ∧ Q2) else P ⊢ (Q1 ★ Q2).
+  sep_destruct : □?p P ⊢ □?p (Q1 ★ Q2).
 Arguments sep_destruct : clear implicits.
 Lemma sep_destruct_spatial p P Q1 Q2 : P ⊢ (Q1 ★ Q2) → SepDestruct p P Q1 Q2.
-Proof. destruct p; simpl=>->; by rewrite ?sep_and. Qed.
+Proof. rewrite /SepDestruct=> ->. by rewrite always_if_sep. Qed.
 
 Global Instance sep_destruct_sep p P Q : SepDestruct p (P ★ Q) P Q.
 Proof. by apply sep_destruct_spatial. Qed.
@@ -737,30 +717,25 @@ Global Instance sep_destruct_ownM p (a b : M) :
 Proof. apply sep_destruct_spatial. by rewrite ownM_op. Qed.
 
 Global Instance sep_destruct_and P Q : SepDestruct true (P ∧ Q) P Q.
-Proof. done. Qed.
+Proof. by rewrite /SepDestruct /= always_and_sep. Qed.
 Global Instance sep_destruct_and_persistent_l P Q :
   PersistentP P → SepDestruct false (P ∧ Q) P Q.
-Proof. intros; red. by rewrite always_and_sep_l. Qed.
+Proof. intros; by rewrite /SepDestruct /= always_and_sep_l. Qed.
 Global Instance sep_destruct_and_persistent_r P Q :
   PersistentP Q → SepDestruct false (P ∧ Q) P Q.
-Proof. intros; red. by rewrite always_and_sep_r. Qed.
+Proof. intros; by rewrite /SepDestruct /= always_and_sep_r. Qed.
 
 Global Instance sep_destruct_later p P Q1 Q2 :
   SepDestruct p P Q1 Q2 → SepDestruct p (▷ P) (▷ Q1) (▷ Q2).
-Proof.
-  destruct p=> /= HP.
-  - by rewrite -later_and !always_later HP.
-  - by rewrite -later_sep HP.
-Qed.
+Proof. by rewrite /SepDestruct -later_sep !always_if_later=> ->. Qed.
 
 Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P)%I → SepDestruct p P P1 P2 →
   envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →
   Δ' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl. destruct p.
-  - by rewrite (sep_destruct true P) right_id (comm uPred_and) wand_elim_r.
-  - by rewrite (sep_destruct false P) right_id (comm uPred_sep P1) wand_elim_r.
+  intros. rewrite envs_simple_replace_sound //; simpl.
+  by rewrite (sep_destruct p P) right_id (comm uPred_sep P1) wand_elim_r.
 Qed.
 
 (** * Framing *)
@@ -850,17 +825,12 @@ Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
   envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 →
   Δ1 ⊢ Q → Δ2 ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros ???? HP1 HP2. rewrite envs_lookup_sound //. destruct p.
-  - rewrite (or_destruct P) always_or sep_or_r; apply or_elim. simpl.
-    + rewrite (envs_simple_replace_sound' _ Δ1) //.
-      by rewrite /= right_id wand_elim_r.
-    + rewrite (envs_simple_replace_sound' _ Δ2) //.
-      by rewrite /= right_id wand_elim_r.
-  - rewrite (or_destruct P) sep_or_r; apply or_elim.
-    + rewrite (envs_simple_replace_sound' _ Δ1) //.
-      by rewrite /= right_id wand_elim_r.
-    + rewrite (envs_simple_replace_sound' _ Δ2) //.
-      by rewrite /= right_id wand_elim_r.
+  intros ???? HP1 HP2. rewrite envs_lookup_sound //.
+  rewrite (or_destruct P) always_if_or sep_or_r; apply or_elim.
+  - rewrite (envs_simple_replace_sound' _ Δ1) //.
+    by rewrite /= right_id wand_elim_r.
+  - rewrite (envs_simple_replace_sound' _ Δ2) //.
+    by rewrite /= right_id wand_elim_r.
 Qed.
 
 (** * Forall *)
@@ -884,9 +854,8 @@ Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
   envs_simple_replace i p (Esnoc Enil i (happly Φ xs)) Δ = Some Δ' →
   Δ' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl. destruct p.
-  - by rewrite right_id (forall_specialize _ P) wand_elim_r.
-  - by rewrite right_id (forall_specialize _ P) wand_elim_r.
+  intros. rewrite envs_simple_replace_sound //; simpl.
+  by rewrite right_id (forall_specialize _ P) wand_elim_r.
 Qed.
 
 Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
@@ -920,15 +889,10 @@ Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q :
     envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ' ∧ Δ' ⊢ Q) →
   Δ ⊢ Q.
 Proof.
-  intros ?? HΦ. rewrite envs_lookup_sound //. destruct p.
-  - rewrite (exist_destruct P) always_exist sep_exist_r.
-    apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
-    rewrite envs_simple_replace_sound' //; simpl.
-    by rewrite right_id wand_elim_r.
-  - rewrite (exist_destruct P) sep_exist_r.
-    apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
-    rewrite envs_simple_replace_sound' //; simpl.
-    by rewrite right_id wand_elim_r.
+  intros ?? HΦ. rewrite envs_lookup_sound //.
+  rewrite (exist_destruct P) always_if_exist sep_exist_r.
+  apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
+  rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
 Qed.
 End tactics.
 
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 5989ed41998b8632e8d0084747a12ce7a269c155..f18d41fcb1994a95760c63e522e12e1e04cd9216 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -51,9 +51,8 @@ Lemma tac_pvs_elim Δ Δ' E1 E2 E3 i p P' P Q :
   E2 ⊆ E1 ∪ E3 →
   Δ' ⊢ (|={E2,E3}=> Q) → Δ ⊢ |={E1,E3}=> Q.
 Proof.
-  intros ? -> ?? HQ. rewrite envs_replace_sound //; simpl. destruct p.
-  - by rewrite always_elim right_id pvs_frame_r wand_elim_r HQ pvs_trans.
-  - by rewrite right_id pvs_frame_r wand_elim_r HQ pvs_trans.
+  intros ? -> ?? HQ. rewrite envs_replace_sound //; simpl.
+  by rewrite always_if_elim right_id pvs_frame_r wand_elim_r HQ pvs_trans.
 Qed.
 
 Lemma tac_pvs_elim_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P' P Q Φ :
@@ -72,11 +71,8 @@ Lemma tac_pvs_timeless Δ Δ' E1 E2 i p P Q :
   Δ' ⊢ (|={E1,E2}=> Q) → Δ ⊢ (|={E1,E2}=> Q).
 Proof.
   intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
-  destruct p.
-  - rewrite always_later (pvs_timeless E1 (â–¡ P)%I) pvs_frame_r.
-    by rewrite right_id wand_elim_r HQ pvs_trans; last set_solver.
-  - rewrite (pvs_timeless E1 P) pvs_frame_r right_id wand_elim_r HQ.
-    by rewrite pvs_trans; last set_solver.
+  rewrite always_if_later (pvs_timeless E1 (â–¡?_ P)%I) pvs_frame_r.
+  by rewrite right_id wand_elim_r HQ pvs_trans; last set_solver.
 Qed.
 
 Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :