diff --git a/.gitignore b/.gitignore
index bcc24b9f1fcd26113792589d865c9b46a632afef..e38a0bd599723aa5eafdad96980bc566d075591e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
 *.vo
+*.vio
 *.v.d
 *.glob
 *.cache
diff --git a/_CoqProject b/_CoqProject
index 2793abada3d6f975a9c44ad72b8acceb0f90839c..46417a25346bf0ed913857e8c0c4fff86c301306 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -35,6 +35,7 @@ prelude/decidable.v
 prelude/list.v
 prelude/error.v
 prelude/functions.v
+prelude/hlist.v
 algebra/option.v
 algebra/cmra.v
 algebra/cmra_big_op.v
@@ -72,7 +73,7 @@ program_logic/hoare.v
 program_logic/language.v
 program_logic/ectx_language.v
 program_logic/ectxi_language.v
-program_logic/ectx_weakestpre.v
+program_logic/ectx_lifting.v
 program_logic/ghost_ownership.v
 program_logic/global_functor.v
 program_logic/saved_prop.v
diff --git a/algebra/upred.v b/algebra/upred.v
index e0a9e313f742e61905f5463b5115a1cb5a02c0d8..c69ac0146f33f0ee87c837bffbcf20cc24ab3eb6 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -467,8 +467,6 @@ Lemma const_elim φ Q R : Q ⊢ ■ φ → (φ → Q ⊢ R) → Q ⊢ R.
 Proof.
   unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
 Qed.
-Lemma False_elim P : False ⊢ P.
-Proof. by unseal; split=> n x ?. Qed.
 Lemma and_elim_l P Q : (P ∧ Q) ⊢ P.
 Proof. by unseal; split=> n x ? [??]. Qed.
 Lemma and_elim_r P Q : (P ∧ Q) ⊢ Q.
@@ -496,7 +494,7 @@ Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ (∃ a, Ψ a).
 Proof. unseal; split=> n x ??; by exists a. Qed.
 Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
 Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
-Lemma eq_refl {A : cofeT} (a : A) P : P ⊢ (a ≡ a).
+Lemma eq_refl {A : cofeT} (a : A) : True ⊢ (a ≡ a).
 Proof. unseal; by split=> n x ??; simpl. Qed.
 Lemma eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P
   `{HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : P ⊢ (a ≡ b) → P ⊢ Ψ a → P ⊢ Ψ b.
@@ -512,6 +510,8 @@ Proof.
 Qed.
 
 (* Derived logical stuff *)
+Lemma False_elim P : False ⊢ P.
+Proof. by apply (const_elim False). Qed.
 Lemma True_intro P : P ⊢ True.
 Proof. by apply const_intro. Qed.
 Lemma and_elim_l' P Q R : P ⊢ R → (P ∧ Q) ⊢ R.
@@ -679,10 +679,13 @@ Lemma const_elim_r φ Q R : (φ → Q ⊢ R) → (Q ∧ ■ φ) ⊢ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
 Lemma const_equiv (φ : Prop) : φ → (■ φ) ⊣⊢ True.
 Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
+Lemma eq_refl' {A : cofeT} (a : A) P : P ⊢ (a ≡ a).
+Proof. rewrite (True_intro P). apply eq_refl. Qed.
+Hint Resolve eq_refl'.
 Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ (a ≡ b).
-Proof. intros ->; apply eq_refl. Qed.
+Proof. by intros ->. Qed.
 Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊢ (b ≡ a).
-Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto using eq_refl. solve_proper. Qed.
+Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed.
 
 (* BI connectives *)
 Lemma sep_mono P P' Q Q' : P ⊢ Q → P' ⊢ Q' → (P ★ P') ⊢ (Q ★ Q').
@@ -898,7 +901,7 @@ Proof.
   apply (anti_symm (⊢)); auto using always_elim.
   apply (eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
   { intros n; solve_proper. }
-  rewrite -(eq_refl a True) always_const; auto.
+  rewrite -(eq_refl a) always_const; auto.
 Qed.
 Lemma always_and_sep P Q : (□ (P ∧ Q)) ⊣⊢ (□ (P ★ Q)).
 Proof. apply (anti_symm (⊢)); auto using always_and_sep_1. Qed.
@@ -1174,5 +1177,5 @@ Hint Resolve and_intro and_elim_l' and_elim_r' : I.
 Hint Resolve always_mono : I.
 Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
 Hint Immediate True_intro False_elim : I.
-Hint Immediate iff_refl eq_refl : I.
+Hint Immediate iff_refl eq_refl' : I.
 End uPred.
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index ac9b0fa0d82eafbab8fb357de536c5ece162d9b6..2c7b17090790ce889c1c5804a004b6aae3f53b13 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -20,7 +20,7 @@ Implicit Types Φ : val → iProp heap_lang Σ.
 Lemma wp_lam E x ef e v Φ :
   to_val e = Some v →
   ▷ WP subst' x e ef @ E {{ Φ }} ⊢ WP App (Lam x ef) e @ E {{ Φ }}.
-Proof. intros. by rewrite -wp_rec. Qed.
+Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
 
 Lemma wp_let E x e1 e2 v Φ :
   to_val e1 = Some v →
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 1b4177494221e41395393308c1869cfc793a70c6..5de7c10d8b5def0132ea3448e80534e2ee72279d 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -120,8 +120,7 @@ Section heap.
   Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
   Proof. rewrite /heap_mapsto. apply _. Qed.
 
-  Lemma heap_mapsto_op_eq l q1 q2 v :
-    (l ↦{q1} v ★ l ↦{q2} v) ⊣⊢ (l ↦{q1+q2} v).
+  Lemma heap_mapsto_op_eq l q1 q2 v : (l ↦{q1} v ★ l ↦{q2} v) ⊣⊢ l ↦{q1+q2} v.
   Proof. by rewrite -auth_own_op op_singleton Frac_op dec_agree_idemp. Qed.
 
   Lemma heap_mapsto_op l q1 q2 v1 v2 :
@@ -135,8 +134,7 @@ Section heap.
     rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
   Qed.
 
-  Lemma heap_mapsto_op_split l q v :
-    (l ↦{q} v) ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
+  Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
   Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
 
   (** Weakest precondition *)
@@ -146,10 +144,8 @@ Section heap.
   Proof.
     iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
     iPvs (auth_empty heap_name) as "Hheap".
-    (* TODO: change [auth_fsa] to single turnstile and use [iApply] *)
-    apply (auth_fsa heap_inv (wp_fsa (Alloc e)))
-      with N heap_name ∅; simpl; eauto with I.
-    iFrame "Hheap". iIntros {h}. rewrite [∅ ⋅ h]left_id.
+    iApply (auth_fsa heap_inv (wp_fsa (Alloc e)) _ N); simpl; eauto.
+    iFrame "Hinv Hheap". iIntros {h}. rewrite [∅ ⋅ h]left_id.
     iIntros "[% Hheap]". rewrite /heap_inv.
     iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
     iIntros {l} "[% Hheap]". iExists (op {[ l := Frac 1 (DecAgree v) ]}), _, _.
@@ -162,66 +158,57 @@ Section heap.
 
   Lemma wp_load N E l q v Φ :
     nclose N ⊆ E →
-    (heap_ctx N ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
+    (heap_ctx N ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v))
+    ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
   Proof.
-    iIntros {?} "[#Hinv [Hmapsto HΦ]]". rewrite /heap_ctx /heap_mapsto.
-    apply (auth_fsa' heap_inv (wp_fsa _) id)
-      with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto with I.
-    iFrame "Hmapsto". iIntros {h} "[% Hheap]". rewrite /heap_inv.
+    iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
+    iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
+      heap_name {[ l := Frac q (DecAgree v) ]}); simpl; eauto.
+    iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
-    rewrite of_heap_singleton_op //. iFrame "Hheap". iNext.
+    rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
     iIntros "$". by iSplit.
   Qed.
 
-  Lemma wp_store N E l v' e v P Φ :
-    to_val e = Some v →
-    P ⊢ heap_ctx N → nclose N ⊆ E →
-    P ⊢ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) →
-    P ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
+  Lemma wp_store N E l v' e v Φ :
+    to_val e = Some v → nclose N ⊆ E →
+    (heap_ctx N ★ ▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit)))
+    ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
-    rewrite /heap_ctx /heap_inv=> ??? HPΦ.
-    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
-      with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
-    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc; apply const_elim_sep_l=> ?.
-    rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
-    rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
-    rewrite const_equiv; last naive_solver.
-    apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
+    iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
+    iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l) _
+      N _ heap_name {[ l := Frac 1 (DecAgree v') ]}); simpl; eauto.
+    iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+    iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
+    rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
+    iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
   Qed.
 
-  Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 P Φ :
-    to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
-    P ⊢ heap_ctx N → nclose N ⊆ E →
-    P ⊢ (▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))) →
-    P ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ :
+    to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose N ⊆ E →
+    (heap_ctx N ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false))))
+    ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    rewrite /heap_ctx /heap_inv=>????? HPΦ.
-    apply (auth_fsa' heap_inv (wp_fsa _) id)
-      with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10 with I.
-    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc; apply const_elim_sep_l=> ?.
-    rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
-    rewrite const_equiv // left_id.
-    rewrite /heap_inv !of_heap_singleton_op //.
-    apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
+    iIntros {????} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
+    iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
+      heap_name {[ l := Frac q (DecAgree v') ]}); simpl; eauto 10.
+    iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+    iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
+    rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
+    iIntros "$". by iSplit.
   Qed.
 
-  Lemma wp_cas_suc N E l e1 v1 e2 v2 P Φ :
-    to_val e1 = Some v1 → to_val e2 = Some v2 →
-    P ⊢ heap_ctx N → nclose N ⊆ E →
-    P ⊢ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) →
-    P ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  Lemma wp_cas_suc N E l e1 v1 e2 v2 Φ :
+    to_val e1 = Some v1 → to_val e2 = Some v2 → nclose N ⊆ E →
+    (heap_ctx N ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true))))
+    ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    rewrite /heap_ctx /heap_inv=> ???? HPΦ.
-    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
-      with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10 with I.
-    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc; apply const_elim_sep_l=> ?.
-    rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) //;
-      last by rewrite lookup_insert.
-    rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
-    rewrite lookup_insert const_equiv; last naive_solver.
-    apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
+    iIntros {???} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
+    iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l)
+      _ N _ heap_name {[ l := Frac 1 (DecAgree v1) ]}); simpl; eauto 10.
+    iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+    iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
+    rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
+    iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
   Qed.
 End heap.
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 153c1f3e2dcac71c3a72f7d9f9841b93fdb9922c..23277892d937dd0f523ecf2efb51671981459862 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -119,8 +119,6 @@ Arguments PairV _%V _%V.
 Arguments InjLV _%V.
 Arguments InjRV _%V.
 
-Definition signal : val := RecV BAnon (BNamed "x") (Store (Var "x") (Lit (LitInt 1))).
-
 Fixpoint of_val (v : val) : expr [] :=
   match v with
   | RecV f x e => Rec f x e
diff --git a/heap_lang/lib/barrier/barrier.v b/heap_lang/lib/barrier/barrier.v
index d8e4a6618c5d54172c91b48ebbbf5d69a65e7b21..b3b5902ff78e354ed8fb17153283c40c6b3071fa 100644
--- a/heap_lang/lib/barrier/barrier.v
+++ b/heap_lang/lib/barrier/barrier.v
@@ -4,3 +4,4 @@ Definition newbarrier : val := λ: <>, ref #0.
 Definition signal : val := λ: "x", '"x" <- #1.
 Definition wait : val :=
   rec: "wait" "x" := if: !'"x" = #1 then #() else '"wait" '"x".
+Global Opaque newbarrier signal wait.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index c79e96fa1f32a63552550e5655304300c41d3d7e..95edcac58535cde750b1e9797c141aec66c5c283 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -82,14 +82,14 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
   ⊢ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))).
 Proof.
   iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
-  iDestruct (big_sepS_delete _ _ i) "HΨ" as "[#HΨi HΨ]"; first done.
+  iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
   iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
-  - iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
-    iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize "HPΨ" "HP". 
-    iDestruct (big_sepS_delete _ _ i) "HPΨ" as "[HΨ HPΨ]"; first done.
-    iDestruct "HQR" "HΨ" as "[HR1 HR2]".
-    rewrite !big_sepS_insert''; [|set_solver ..]. by iFrame "HR1 HR2".
-  - rewrite !big_sepS_insert'; [|set_solver ..]. by repeat iSplit.
+  - iPoseProof (saved_prop_agree i Q (Ψ i) with "#") as "Heq"; first by iSplit.
+    iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
+    iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
+    iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
+    rewrite !big_sepS_insert''; [|abstract set_solver ..]. by iFrame "HR1 HR2".
+  - rewrite !big_sepS_insert'; [|abstract set_solver ..]. by repeat iSplit.
 Qed.
 
 (** Actual proofs *)
@@ -102,8 +102,8 @@ Proof.
   rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
   iApply "HΦ".
   iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
-  iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}))
-    "-" as {γ'} "[#? Hγ']"; eauto.
+  iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "-")
+    as {γ'} "[#? Hγ']"; eauto.
   { iNext. rewrite /barrier_inv /=. iFrame "Hl".
     iExists (const P). rewrite !big_sepS_singleton /=.
     iSplit; [|done]. by iIntros "> ?". }
@@ -113,9 +113,9 @@ Proof.
     ★ sts_ownS γ' low_states {[Send]})%I as "[Hr Hs]" with "-".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     + set_solver.
-    + iApply sts_own_weaken "Hγ'";
+    + iApply (sts_own_weaken with "Hγ'");
         auto using sts.closed_op, i_states_closed, low_states_closed;
-        set_solver. }
+        abstract set_solver. }
   iPvsIntro. rewrite /recv /send. iSplitL "Hr".
   - iExists γ', P, P, γ. iFrame "Hr". repeat iSplit; auto. by iIntros "> ?".
   - iExists γ'. by iSplit.
@@ -132,7 +132,7 @@ Proof.
   iSplit; [iPureIntro; by eauto using signal_step|].
   iSplitR "HΦ"; [iNext|by iIntros "?"].
   rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
-  iDestruct "Hr" as {Ψ} "[? Hsp]"; iExists Ψ; iFrame "Hsp".
+  iDestruct "Hr" as {Ψ} "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
   iIntros "> _"; by iApply "Hr".
 Qed.
 
@@ -149,20 +149,20 @@ Proof.
     { iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". }
     iIntros "Hγ".
     iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I as "Hγ" with "[Hγ]".
-    { iApply sts_own_weaken "Hγ"; eauto using i_states_closed. }
-    wp_op=> ?; simplify_eq; wp_if. iApply "IH" "Hγ [HQR] HΦ". by iNext.
+    { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
+    wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). by iNext.
   - (* a High state: the comparison succeeds, and we perform a transition and
     return to the client *)
     iExists (State High (I ∖ {[ i ]})), (∅ : set token).
     iSplit; [iPureIntro; by eauto using wait_step|].
     iDestruct "Hr" as {Ψ} "[HΨ Hsp]".
-    iDestruct (big_sepS_delete _ _ i) "Hsp" as "[#HΨi Hsp]"; first done.
+    iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
     iAssert (▷ Ψ i ★ ▷ Π★{set (I ∖ {[i]})} Ψ)%I as "[HΨ HΨ']" with "[HΨ]".
     { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
     iSplitL "HΨ' Hl Hsp"; [iNext|].
     + rewrite {2}/barrier_inv /=; iFrame "Hl".
       iExists Ψ; iFrame "Hsp". by iIntros "> _".
-    + iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
+    + iPoseProof (saved_prop_agree i Q (Ψ i) with "#") as "Heq"; first by iSplit.
       iIntros "_". wp_op=> ?; simplify_eq/=; wp_if.
       iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
 Qed.
@@ -176,7 +176,7 @@ Proof.
   iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
   iPvs (saved_prop_alloc_strong _ (R1: ∙%CF iProp) I) as {i1} "[% #Hi1]".
   iPvs (saved_prop_alloc_strong _ (R2: ∙%CF iProp) (I ∪ {[i1]}))
-    as {i2} "[Hi2' #Hi2]"; iPure "Hi2'" as Hi2; iPvsIntro.
+    as {i2} "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2; iPvsIntro.
   rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
   iExists (State p ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]})))).
   iExists ({[Change i1 ]} ∪ {[ Change i2 ]}).
@@ -188,8 +188,9 @@ Proof.
       ★ sts_ownS γ (i_states i2) {[Change i2]})%I as "[Hγ1 Hγ2]" with "-".
     { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
       + set_solver.
-      + iApply sts_own_weaken "Hγ"; eauto using sts.closed_op, i_states_closed.
-        set_solver. }
+      + iApply (sts_own_weaken with "Hγ");
+          eauto using sts.closed_op, i_states_closed.
+        abstract set_solver. }
     iPvsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
     + iExists γ, P, R1, i1. iFrame "Hγ1 Hi1". repeat iSplit; auto.
       by iIntros "> ?".
@@ -205,8 +206,7 @@ Proof.
   iIntros "> HQ". by iApply "HP"; iApply "HP1".
 Qed.
 
-Lemma recv_mono l P1 P2 :
-  P1 ⊢ P2 → recv l P1 ⊢ recv l P2.
+Lemma recv_mono l P1 P2 : P1 ⊢ P2 → recv l P1 ⊢ recv l P2.
 Proof.
   intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
 Qed.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 09bec1ec5c30000c106d9d54ef879934cb46ca87..df476fbf411578ea71696da13e268aa756cb5c44 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -5,8 +5,10 @@ Import uPred.
 
 Definition newlock : val := λ: <>, ref #false.
 Definition acquire : val :=
-  rec: "lock" "l" := if: CAS '"l" #false #true then #() else '"lock" '"l".
+  rec: "acquire" "l" :=
+    if: CAS '"l" #false #true then #() else '"acquire" '"l".
 Definition release : val := λ: "l", '"l" <- #false.
+Global Opaque newlock acquire release.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
@@ -55,8 +57,8 @@ Proof.
   iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
   wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
   iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
-  iPvs (inv_alloc N _ (lock_inv γ l R)) "-[HΦ]" as "#?"; first done.
-  { iNext. iExists false. by iFrame "Hl HR". }
+  iPvs (inv_alloc N _ (lock_inv γ l R) with "-[HΦ]") as "#?"; first done.
+  { iIntros ">". iExists false. by iFrame "Hl HR". }
   iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit.
 Qed.
 
@@ -65,23 +67,20 @@ Lemma acquire_spec l R (Φ : val → iProp) :
 Proof.
   iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
   iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
-  iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl HR]"; destruct b.
+  iInv N as { [] } "[Hl HR]".
   - wp_cas_fail. iSplitL "Hl".
     + iNext. iExists true. by iSplit.
     + wp_if. by iApply "IH".
   - wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
     + iNext. iExists true. by iSplit.
-    + wp_if. iPvsIntro. iApply "HΦ" "-[HR] HR". iExists N, γ. by repeat iSplit.
+    + wp_if. iApply ("HΦ" with "-[HR] HR"). iExists N, γ. by repeat iSplit.
 Qed.
 
 Lemma release_spec R l (Φ : val → iProp) :
   (locked l R ★ R ★ Φ #()) ⊢ WP release #l {{ Φ }}.
 Proof.
-  iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(%&#?&#?&Hγ)".
-  rewrite /release. wp_let.
-  iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl Hγ']"; destruct b.
-  - wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
-  - wp_store. iDestruct "Hγ'" as "[Hγ' _]".
-    iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%".
+  iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)".
+  rewrite /release. wp_let. iInv N as {b} "[Hl _]".
+  wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
 Qed.
 End proof.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 12d3c18c0943c8d45c8aa3fdd6aba341c54d01b4..e394bfc471b923bde4958c6c39aa9f8c97021fb6 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -14,7 +14,7 @@ Infix "||" := Par : expr_scope.
 Instance do_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
 Instance do_wsubst_par {X Y} x es (H : X `included` x :: Y) :
   WSubst x es H par par := do_wsubst_closed _ x es H _.
-Typeclasses Opaque par.
+Global Opaque par.
 
 Section proof.
 Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
@@ -32,7 +32,7 @@ Proof.
   iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _).
   iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let.
   wp_apply join_spec; iFrame "Hl". iIntros {w} "H1".
-  iSpecialize "HΦ" "-"; first by iSplitL "H1". by wp_let.
+  iSpecialize ("HΦ" with "* -"); first by iSplitL "H1". by wp_let.
 Qed.
 
 Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 454c1489cb8f73f6b127d869351ef06b270d1e24..b2f5f24beb19b4def7281d5370c93c726446a98c 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -13,6 +13,7 @@ Definition join : val :=
       InjR "x" => '"x"
     | InjL <>  => '"join" '"c"
     end.
+Global Opaque spawn join.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
@@ -57,15 +58,15 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
   ⊢ WP spawn e {{ Φ }}.
 Proof.
   iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
-  wp_let; wp_alloc l as "Hl"; wp_let.
+  wp_let. wp_alloc l as "Hl". wp_let.
   iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
-  iPvs (inv_alloc N _ (spawn_inv γ l Ψ)) "[Hl]" as "#?"; first done.
+  iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
   { iNext. iExists (InjLV #0). iFrame "Hl". by iLeft. }
   wp_apply wp_fork. iSplitR "Hf".
-  - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. iSplit; first done.
-    iExists γ. iFrame "Hγ"; by iSplit.
+  - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle.
+    iSplit; first done. iExists γ. iFrame "Hγ"; by iSplit.
   - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
-    iInv N as "Hinv"; first wp_done; iDestruct "Hinv" as {v'} "[Hl _]".
+    iInv N as {v'} "[Hl _]"; first wp_done.
     wp_store. iSplit; [iNext|done].
     iExists (InjRV v); iFrame "Hl"; iRight; iExists v; iSplit; [done|by iLeft].
 Qed.
@@ -74,17 +75,16 @@ Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
   (join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v) ⊢ WP join #l {{ Φ }}.
 Proof.
   rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
-  iLöb as "IH". wp_rec. wp_focus (! _)%E.
-  iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]".
+  iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|].
-    wp_case. wp_seq. iApply "IH" "Hγ Hv".
+    wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
   - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
     + iSplitL "Hl Hγ".
       { iNext. iExists _; iFrame "Hl"; iRight.
         iExists _; iSplit; [done|by iRight]. }
       wp_case. wp_let. iPvsIntro. by iApply "Hv".
-    + iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%".
+    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
 Qed.
 End proof.
 
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 157125e2249b2a7679d68a38a70b3e82e56b6e2c..b81fac90182c46ddd3fa72b1dc5a4bfb7374d4ae 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
-From iris.program_logic Require Export ectx_weakestpre.
-From iris.program_logic Require Import ownership. (* for ownP *)
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import weakestpre.
@@ -86,22 +86,16 @@ Proof.
   rewrite later_sep -(wp_value _ _ (Lit _)) //.
 Qed.
 
-Lemma wp_rec E f x e1 e2 v Φ :
-  to_val e2 = Some v →
-  ▷ WP subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
-  ⊢ WP App (Rec f x e1) e2 @ E {{ Φ }}.
-Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (App _ _)
-    (subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id;
-    intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_rec' E f x erec e1 e2 v2 Φ :
+Lemma wp_rec E f x erec e1 e2 v2 Φ :
   e1 = Rec f x erec →
   to_val e2 = Some v2 →
   ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
   ⊢ WP App e1 e2 @ E {{ Φ }}.
-Proof. intros ->. apply wp_rec. Qed.
+Proof.
+  intros -> ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
+    (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
+    intros; inv_head_step; eauto.
+Qed.
 
 Lemma wp_un_op E op l l' Φ :
   un_op_eval op l = Some l' →
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 3a6884ecbf9b341f6a372ddeae8daa3c2482f9af..cf0c7db5c98facdcee53ffcea03c8b3012af9eee 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -33,7 +33,7 @@ Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
 Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
 
 Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
-Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
+Notation "^ e" := (wexpr' e) (at level 8, format "^ e") : expr_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index ffd83b20b83c0337377e87585c3345bb9ed1e204..b57a9ea5c718ca8e51db4d7a986d7d6ff65169fa 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -52,7 +52,7 @@ Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
   Δ'' ⊢ Φ (LitV LitUnit) → Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
-  intros. eapply wp_store; eauto.
+  intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
   rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -65,114 +65,134 @@ Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
   Δ' ⊢ Φ (LitV (LitBool false)) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. eapply wp_cas_fail; eauto.
+  intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
   rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l e1 v1 e2 v2 Φ :
+Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   Δ ⊢ heap_ctx N → nclose N ⊆ E →
   StripLaterEnvs Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦ v1)%I →
+  envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   Δ'' ⊢ Φ (LitV (LitBool true)) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. eapply wp_cas_suc; eauto.
+  intros; subst.
+  rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
   rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     wp_bind K; iApply lem; try iNext)
-  end.
-
-Tactic Notation "wp_apply" open_constr(lem) constr(Hs) :=
-  match goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind K; iApply lem Hs; try iNext)
+  | _ => fail "wp_apply: not a 'wp'"
   end.
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
-  match goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | Alloc ?e =>
-       wp_bind K; eapply tac_wp_alloc with _ _ H _;
-         [wp_done || fail 2 "wp_alloc:" e "not a value"
-         |iAssumption || fail 2 "wp_alloc: cannot find heap_ctx"
-         |done || eauto with ndisj
-         |apply _
-         |intros l; eexists; split;
-           [env_cbv; reflexivity || fail 2 "wp_alloc:" H "not fresh"
-           |wp_finish]]
-    end)
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with Alloc _ => wp_bind K end)
+      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+    eapply tac_wp_alloc with _ _ H _;
+      [let e' := match goal with |- to_val ?e' = _ => e' end in
+       wp_done || fail "wp_alloc:" e' "not a value"
+      |iAssumption || fail "wp_alloc: cannot find heap_ctx"
+      |done || eauto with ndisj
+      |apply _
+      |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
+        eexists; split;
+          [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
+          |wp_finish]]
+  | _ => fail "wp_alloc: not a 'wp'"
   end.
-Tactic Notation "wp_alloc" ident(l) := let H := iFresh in wp_alloc l as H.
+
+Tactic Notation "wp_alloc" ident(l) :=
+  let H := iFresh in wp_alloc l as H.
 
 Tactic Notation "wp_load" :=
-  match goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | Load (Lit (LitLoc ?l)) =>
-       wp_bind K; eapply tac_wp_load;
-         [iAssumption || fail 2 "wp_load: cannot find heap_ctx"
-         |done || eauto with ndisj
-         |apply _
-         |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
-         |wp_finish]
-    end)
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with Load _ => wp_bind K end)
+      |fail 1 "wp_load: cannot find 'Load' in" e];
+    eapply tac_wp_load;
+      [iAssumption || fail "wp_load: cannot find heap_ctx"
+      |done || eauto with ndisj
+      |apply _
+      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+       iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
+      |wp_finish]
+  | _ => fail "wp_load: not a 'wp'"
   end.
 
 Tactic Notation "wp_store" :=
-  match goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | Store ?l ?e =>
-       wp_bind K; eapply tac_wp_store;
-         [wp_done || fail 2 "wp_store:" e "not a value"
-         |iAssumption || fail 2 "wp_store: cannot find heap_ctx"
-         |done || eauto with ndisj
-         |apply _
-         |iAssumptionCore || fail 2 "wp_store: cannot find" l "↦ ?"
-         |env_cbv; reflexivity
-         |wp_finish]
-    end)
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with Store _ _ => wp_bind K end)
+      |fail 1 "wp_store: cannot find 'Store' in" e];
+    eapply tac_wp_store;
+      [let e' := match goal with |- to_val ?e' = _ => e' end in
+       wp_done || fail "wp_store:" e' "not a value"
+      |iAssumption || fail "wp_store: cannot find heap_ctx"
+      |done || eauto with ndisj
+      |apply _
+      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+       iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
+      |env_cbv; reflexivity
+      |wp_finish]
+  | _ => fail "wp_store: not a 'wp'"
   end.
 
 Tactic Notation "wp_cas_fail" :=
-  match goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | CAS (Lit (LitLoc ?l)) ?e1 ?e2 =>
-       wp_bind K; eapply tac_wp_cas_fail;
-         [wp_done || fail 2 "wp_cas_fail:" e1 "not a value"
-         |wp_done || fail 2 "wp_cas_fail:" e2 "not a value"
-         |iAssumption || fail 2 "wp_cas_fail: cannot find heap_ctx"
-         |done || eauto with ndisj
-         |apply _
-         |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
-         |try discriminate
-         |wp_finish]
-    end)
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with CAS _ _ _ => wp_bind K end)
+      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
+    eapply tac_wp_cas_fail;
+      [let e' := match goal with |- to_val ?e' = _ => e' end in
+       wp_done || fail "wp_cas_fail:" e' "not a value"
+      |let e' := match goal with |- to_val ?e' = _ => e' end in
+       wp_done || fail "wp_cas_fail:" e' "not a value"
+      |iAssumption || fail "wp_cas_fail: cannot find heap_ctx"
+      |done || eauto with ndisj
+      |apply _
+      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+       iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
+      |try congruence
+      |wp_finish]
+  | _ => fail "wp_cas_fail: not a 'wp'"
   end.
 
 Tactic Notation "wp_cas_suc" :=
-  match goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with
-    | CAS (Lit (LitLoc ?l)) ?e1 ?e2 =>
-       wp_bind K; eapply tac_wp_cas_suc;
-         [wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
-         |wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
-         |iAssumption || fail 2 "wp_cas_suc: cannot find heap_ctx"
-         |done || eauto with ndisj
-         |apply _
-         |iAssumptionCore || fail 2 "wp_cas_suc: cannot find" l "↦ ?"
-         |env_cbv; reflexivity
-         |wp_finish]
-    end)
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         match eval hnf in e' with CAS _ _ _ => wp_bind K end)
+      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
+    eapply tac_wp_cas_suc;
+      [let e' := match goal with |- to_val ?e' = _ => e' end in
+       wp_done || fail "wp_cas_suc:" e' "not a value"
+      |let e' := match goal with |- to_val ?e' = _ => e' end in
+       wp_done || fail "wp_cas_suc:" e' "not a value"
+      |iAssumption || fail "wp_cas_suc: cannot find heap_ctx"
+      |done || eauto with ndisj
+      |apply _
+      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+       iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
+      |try congruence
+      |env_cbv; reflexivity
+      |wp_finish]
+  | _ => fail "wp_cas_suc: not a 'wp'"
   end.
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index e8da21dfe79718c39223652252c24325f0c8584b..75ea52bef9f13ad4486746b4bac00e28441ba0d6 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -2,8 +2,7 @@ From iris.heap_lang Require Export lang.
 Import heap_lang.
 
 (** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
-can be tuned using instances of the type class [Closed e], which can be used
-to mark that expressions are closed, and should thus not be substituted into. *)
+can be tuned by declaring [WExpr] and [WSubst] instances. *)
 
 (** * Weakening *)
 Class WExpr {X Y} (H : X `included` Y) (e : expr X) (er : expr Y) :=
@@ -16,22 +15,18 @@ Hint Extern 0 (WExpr _ (Var ?y) _) =>
 
 (* Rec *)
 Instance do_wexpr_rec_true {X Y f y e} {H : X `included` Y} er :
-  WExpr (wexpr_rec_prf H) e er → WExpr H (Rec f y e) (Rec f y er).
+  WExpr (wexpr_rec_prf H) e er → WExpr H (Rec f y e) (Rec f y er) | 10.
 Proof. intros; red; f_equal/=. by etrans; [apply wexpr_proof_irrel|]. Qed.
 
 (* Values *)
-Instance do_wexpr_of_val_nil (H : [] `included` []) v :
-  WExpr H (of_val v) (of_val v) | 0.
+Instance do_wexpr_wexpr X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) e er :
+  WExpr (transitivity H1 H2) e er → WExpr H2 (wexpr H1 e) er | 0.
+Proof. by rewrite /WExpr wexpr_wexpr'. Qed.
+Instance do_wexpr_closed_closed (H : [] `included` []) e : WExpr H e e | 1.
 Proof. apply wexpr_id. Qed.
-Instance do_wexpr_of_val_nil' X (H : X `included` []) v :
-  WExpr H (of_val' v) (of_val v) | 0.
-Proof. by rewrite /WExpr /of_val' wexpr_wexpr' wexpr_id. Qed.
-Instance do_wexpr_of_val Y (H : [] `included` Y) v :
-  WExpr H (of_val v) (of_val' v) | 1.
+Instance do_wexpr_closed_wexpr Y (H : [] `included` Y) e :
+  WExpr H e (wexpr' e) | 2.
 Proof. apply wexpr_proof_irrel. Qed.
-Instance do_wexpr_of_val' X Y (H : X `included` Y) v :
-  WExpr H (of_val' v) (of_val' v) | 1.
-Proof. apply wexpr_wexpr. Qed.
 
 (* Boring connectives *)
 Section do_wexpr.
@@ -129,32 +124,16 @@ Hint Extern 0 (WSubst ?x ?v _ (Rec ?f ?y ?e) _) =>
   end : typeclass_instances.
 
 (* Values *)
-Instance do_wsubst_of_val_nil x es (H : [] `included` [x]) w :
-  WSubst x es H (of_val w) (of_val w) | 0.
+Instance do_wsubst_wexpr X Y Z x es
+    (H1 : X `included` Y) (H2 : Y `included` x :: Z) e er :
+  WSubst x es (transitivity H1 H2) e er → WSubst x es H2 (wexpr H1 e) er | 0.
+Proof. by rewrite /WSubst wsubst_wexpr'. Qed.
+Instance do_wsubst_closed_closed x es (H : [] `included` [x]) e :
+  WSubst x es H e e | 1.
 Proof. apply wsubst_closed_nil. Qed.
-Instance do_wsubst_of_val_nil' {X} x es (H : X `included` [x]) w :
-  WSubst x es H (of_val' w) (of_val w) | 0.
-Proof. by rewrite /WSubst /of_val' wsubst_wexpr' wsubst_closed_nil. Qed.
-Instance do_wsubst_of_val Y x es (H : [] `included` x :: Y) w :
-  WSubst x es H (of_val w) (of_val' w) | 1.
+Instance do_wsubst_closed_wexpr Y x es (H : [] `included` x :: Y) e :
+  WSubst x es H e (wexpr' e) | 2.
 Proof. apply wsubst_closed, not_elem_of_nil. Qed.
-Instance do_wsubst_of_val' X Y x es (H : X `included` x :: Y) w :
-  WSubst x es H (of_val' w) (of_val' w) | 1.
-Proof.
-  rewrite /WSubst /of_val' wsubst_wexpr'.
-  apply wsubst_closed, not_elem_of_nil.
-Qed.
-
-(* Closed expressions *)
-Instance do_wsubst_expr_nil' {X} x es (H : X `included` [x]) e :
-  WSubst x es H (wexpr' e) e | 0.
-Proof. by rewrite /WSubst /wexpr' wsubst_wexpr' wsubst_closed_nil. Qed.
-Instance do_wsubst_wexpr' X Y x es (H : X `included` x :: Y) e :
-  WSubst x es H (wexpr' e) (wexpr' e) | 1.
-Proof.
-  rewrite /WSubst /wexpr' wsubst_wexpr'.
-  apply wsubst_closed, not_elem_of_nil.
-Qed.
 
 (* Boring connectives *)
 Section wsubst.
@@ -216,5 +195,3 @@ Ltac simpl_subst :=
 Arguments wexpr : simpl never.
 Arguments subst : simpl never.
 Arguments wsubst : simpl never.
-Arguments of_val : simpl never.
-Arguments of_val' : simpl never.
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index 796832ee3f2cb0084f1590d5672e344735751cb4..336f4043f8888ba97b9a8cdffbc1e07bd3f3058b 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -25,7 +25,7 @@ Ltac reshape_val e tac :=
   let rec go e :=
   match e with
   | of_val ?v => v
-  | of_val' ?v => v
+  | wexpr' ?e => reshape_val e tac
   | Rec ?f ?x ?e => constr:(RecV f x e)
   | Lit ?l => constr:(LitV l)
   | Pair ?e1 ?e2 =>
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index dc73a065f7a6f92a26a79c7b16718e1f674abd8f..2411087c3d92d5eaa58f74bca73b7eef1aaa91bf 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -9,7 +9,7 @@ Ltac wp_bind K :=
   | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
   end.
 
-Ltac wp_done := rewrite -/of_val /= ?to_of_val; fast_done.
+Ltac wp_done := rewrite /= ?to_of_val; fast_done.
 
 Ltac wp_value_head :=
   match goal with
@@ -23,12 +23,13 @@ Ltac wp_value_head :=
   end.
 
 Ltac wp_finish := intros_revert ltac:(
-  rewrite -/of_val /= ?to_of_val; try strip_later; try wp_value_head).
+  rewrite /= ?to_of_val; try strip_later; try wp_value_head).
 
 Tactic Notation "wp_value" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind K; wp_value_head)
+    wp_bind K; wp_value_head) || fail "wp_value: cannot find value in" e
+  | _ => fail "wp_value: not a wp"
   end.
 
 Tactic Notation "wp_rec" :=
@@ -37,24 +38,26 @@ Tactic Notation "wp_rec" :=
     match eval hnf in e' with App ?e1 _ =>
 (* hnf does not reduce through an of_val *)
 (*      match eval hnf in e1 with Rec _ _ _ => *)
-    wp_bind K; etrans; [|eapply wp_rec'; wp_done]; simpl_subst; wp_finish
-(*      end *) end)
-   end.
+    wp_bind K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish
+(*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
+  | _ => fail "wp_rec: not a 'wp'"
+  end.
 
 Tactic Notation "wp_lam" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with App ?e1 _ =>
 (*    match eval hnf in e1 with Rec BAnon _ _ => *)
     wp_bind K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
-(*    end *) end)
+(*    end *) end) || fail "wp_lam: cannot find 'Lam' in" e
+  | _ => fail "wp_lam: not a 'wp'"
   end.
 
 Tactic Notation "wp_let" := wp_lam.
 Tactic Notation "wp_seq" := wp_let.
 
 Tactic Notation "wp_op" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
@@ -64,39 +67,48 @@ Tactic Notation "wp_op" :=
        wp_bind K; etrans; [|eapply wp_bin_op; try fast_done]; wp_finish
     | UnOp _ _ =>
        wp_bind K; etrans; [|eapply wp_un_op; try fast_done]; wp_finish
-    end)
+    end) || fail "wp_op: cannot find 'BinOp' or 'UnOp' in" e
+  | _ => fail "wp_op: not a 'wp'"
   end.
 
 Tactic Notation "wp_proj" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Fst _ => wp_bind K; etrans; [|eapply wp_fst; wp_done]; wp_finish
     | Snd _ => wp_bind K; etrans; [|eapply wp_snd; wp_done]; wp_finish
-    end)
+    end) || fail "wp_proj: cannot find 'Fst' or 'Snd' in" e
+  | _ => fail "wp_proj: not a 'wp'"
   end.
 
 Tactic Notation "wp_if" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with If _ _ _ =>
-    wp_bind K;
-    etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
-    end)
+    match eval hnf in e' with
+    | If _ _ _ =>
+      wp_bind K;
+      etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
+    end) || fail "wp_if: cannot find 'If' in" e
+  | _ => fail "wp_if: not a 'wp'"
   end.
 
 Tactic Notation "wp_case" :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval hnf in e' with Case _ _ _ =>
+    match eval hnf in e' with
+    | Case _ _ _ =>
       wp_bind K;
       etrans; [|first[eapply wp_case_inl; wp_done|eapply wp_case_inr; wp_done]];
       wp_finish
-    end)
+    end) || fail "wp_case: cannot find 'Case' in" e
+  | _ => fail "wp_case: not a 'wp'"
   end.
 
 Tactic Notation "wp_focus" open_constr(efoc) :=
-  match goal with
+  lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match e' with efoc => unify e' efoc; wp_bind K end)
+    match e' with
+    | efoc => unify e' efoc; wp_bind K
+    end) || fail "wp_focus: cannot find" efoc "in" e
+  | _ => fail "wp_focus: not a 'wp'"
   end.
diff --git a/prelude/decidable.v b/prelude/decidable.v
index 819749a94b9db14aaef632d3493c16b817ce7e11..76ec221035db68e9da9146cf98d9dd18056e4fc6 100644
--- a/prelude/decidable.v
+++ b/prelude/decidable.v
@@ -180,8 +180,6 @@ Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
   match p as p return Decision (curry P p) with
   | (x,y) => P_dec x y
   end.
-Instance uncurry_dec `(P_dec : ∀ (p : A * B), Decision (P p)) x y :
-  Decision (uncurry P x y) := P_dec (x,y).
 
 Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   `{∀ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
diff --git a/prelude/hlist.v b/prelude/hlist.v
new file mode 100644
index 0000000000000000000000000000000000000000..1f307b0628735395b6d069b0589528425f1c1002
--- /dev/null
+++ b/prelude/hlist.v
@@ -0,0 +1,18 @@
+From iris.prelude Require Import base.
+
+(* Not using [list Type] in order to avoid universe inconsistencies *)
+Inductive tlist := tnil : tlist | tcons : Type → tlist → tlist.
+
+Inductive hlist : tlist → Type :=
+  | hnil : hlist tnil
+  | hcons {A As} : A → hlist As → hlist (tcons A As).
+
+Fixpoint himpl (As : tlist) (B : Type) : Type :=
+  match As with tnil => B | tcons A As => A → himpl As B end.
+
+Definition happly {As B} (f : himpl As B) (xs : hlist As) : B :=
+  (fix go As xs :=
+    match xs in hlist As return himpl As B → B with
+    | hnil => λ f, f
+    | hcons A As x xs => λ f, go As xs (f x)
+    end) _ xs f.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index dc272fe9dfe73ca7e450d58b44b623d6ecb2085a..029e21f172436bbd3ace8354902c64bb29bccc8d 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export auth upred_tactics.
 From iris.program_logic Require Export invariants ghost_ownership.
+From iris.proofmode Require Import invariants ghost_ownership.
 Import uPred.
 
 (* The CMRA we need. *)
@@ -57,100 +58,56 @@ Section auth.
     ✓ a → nclose N ⊆ E →
     ▷ φ a ⊢ (|={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
   Proof.
-    intros Ha HN. eapply sep_elim_True_r.
-    { by eapply (own_alloc (Auth (Excl a) a) E). }
-    rewrite pvs_frame_l. apply pvs_strip_pvs.
-    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
-    trans (▷ auth_inv γ φ ★ auth_own γ a)%I.
-    { rewrite /auth_inv -(exist_intro a) later_sep.
-      ecancel [▷ φ _]%I.
-      by rewrite -later_intro -own_op auth_both_op. }
-    rewrite (inv_alloc N E) // /auth_ctx pvs_frame_r. apply pvs_mono.
-    by rewrite always_and_sep_l.
+    iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
+    iPvs (own_alloc (Auth (Excl a) a)) as {γ} "Hγ"; first done.
+    iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
+    iPvs (inv_alloc N _ (auth_inv γ φ) with "-[Hγ']"); first done.
+    { iNext. iExists a. by iFrame "Hφ". }
+    iPvsIntro; iExists γ; by iFrame "Hγ'".
   Qed.
 
   Lemma auth_empty γ E : True ⊢ |={E}=> auth_own γ ∅.
   Proof. by rewrite -own_empty. Qed.
 
-  Lemma auth_opened E γ a :
-    (▷ auth_inv γ φ ★ auth_own γ a)
-    ⊢ (|={E}=> ∃ a', ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a)).
-  Proof.
-    rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
-    rewrite later_sep [(â–· own _ _)%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
-    rewrite own_valid_l discrete_valid -!assoc. apply const_elim_sep_l=>Hv.
-    rewrite [(▷φ _ ★ _)%I]comm assoc -own_op.
-    rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
-    apply exist_elim=>a'.
-    rewrite left_id -(exist_intro a').
-    apply (eq_rewrite b (a ⋅ a') (λ x, ✓ x ★ ▷ φ x ★ own γ (● x ⋅ ◯ a))%I).
-    { by move=>n x y /timeless_iff ->. }
-    { by eauto with I. }
-    rewrite -valid_intro; last by apply Hv.
-    rewrite left_id comm. auto with I.
-  Qed.
-
-  Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
-    Lv a → ✓ (L a ⋅ a') →
-    (▷ φ (L a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a))
-    ⊢ (|={E}=> ▷ auth_inv γ φ ★ auth_own γ (L a)).
-  Proof.
-    intros HL Hv. rewrite /auth_inv -(exist_intro (L a â‹… a')).
-    (* TODO it would be really nice to use cancel here *)
-    rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
-    rewrite -pvs_frame_l. apply sep_mono_r.
-    rewrite -later_intro -own_op.
-    by apply own_update, (auth_local_update_l L).
-  Qed.
-
   Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
 
-  Lemma auth_fsa E N P (Ψ : V → iPropG Λ Σ) γ a :
-    fsaV →
-    nclose N ⊆ E →
-    P ⊢ auth_ctx γ N φ →
-    P ⊢ (▷ auth_own γ a ★ ∀ a',
-          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
-          fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
-            ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
-            (auth_own γ (L a) -★ Ψ x))) →
-    P ⊢ fsa E Ψ.
+  Lemma auth_fsa E N (Ψ : V → iPropG Λ Σ) γ a :
+    fsaV → nclose N ⊆ E →
+    (auth_ctx γ N φ ★ ▷ auth_own γ a ★ ∀ a',
+      ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+      fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
+        ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
+        (auth_own γ (L a) -★ Ψ x)))
+     ⊢ fsa E Ψ.
   Proof.
-    rewrite /auth_ctx=>? HN Hinv Hinner.
-    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
-    apply wand_intro_l. rewrite assoc.
-    rewrite (pvs_timeless (E ∖ N)) pvs_frame_l pvs_frame_r.
-    apply (fsa_strip_pvs fsa).
-    rewrite (auth_opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
-    apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
-    rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]comm.
-    eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
-    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc discrete_valid.  done. }
-    rewrite fsa_frame_l.
-    apply (fsa_mono_pvs fsa)=> x.
-    rewrite sep_exist_l; apply exist_elim=> L.
-    rewrite sep_exist_l; apply exist_elim=> Lv.
-    rewrite sep_exist_l; apply exist_elim=> ?.
-    rewrite comm -!assoc. apply const_elim_sep_l=>-[HL Hv].
-    rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc.
-    rewrite (auth_closing (E ∖ N)) //; [].
-    rewrite pvs_frame_l. apply pvs_mono.
-    by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
+    iIntros {??} "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
+    iInv N as {a'} "[Hγ Hφ]".
+    iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
+    iDestruct (own_valid _ with "Hγ !") as "Hvalid".
+    iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
+    iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
+    rewrite ->(left_id _ _) in Ha'; setoid_subst.
+    iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
+    { iApply "HΨ"; by iSplit. }
+    iIntros {v} "HL". iDestruct "HL" as {L Lv ?} "(% & Hφ & HΨ)".
+    iPvs (own_update _ with "Hγ") as "[Hγ Hγf]".
+    { apply (auth_local_update_l L); tauto. }
+    iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
+    iNext. iExists (L a ⋅ b). by iFrame "Hφ".
   Qed.
-  Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Ψ : V → iPropG Λ Σ) γ a :
-    fsaV →
-    nclose N ⊆ E →
-    P ⊢ auth_ctx γ N φ →
-    P ⊢ (▷ auth_own γ a ★ (∀ a',
-          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
-          fsa (E ∖ nclose N) (λ x,
-            ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
-            (auth_own γ (L a) -★ Ψ x)))) →
-    P ⊢ fsa E Ψ.
+
+  Lemma auth_fsa' L `{!LocalUpdate Lv L} E N (Ψ : V → iPropG Λ Σ) γ a :
+    fsaV → nclose N ⊆ E →
+    (auth_ctx γ N φ ★ ▷ auth_own γ a ★ (∀ a',
+      ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+      fsa (E ∖ nclose N) (λ x,
+        ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
+        (auth_own γ (L a) -★ Ψ x))))
+    ⊢ fsa E Ψ.
   Proof.
-    intros ??? HP. eapply auth_fsa with N γ a; eauto.
-    rewrite HP; apply sep_mono_r, forall_mono=> a'.
-    apply wand_mono; first done. apply (fsa_mono fsa)=> b.
-    rewrite -(exist_intro L). by repeat erewrite <-exist_intro by apply _.
+    iIntros {??} "(#Ha & Hγf & HΨ)"; iApply (auth_fsa E N Ψ γ a); auto.
+    iFrame "Ha Hγf". iIntros {a'} "H".
+    iApply fsa_wand_r; iSplitL; first by iApply "HΨ".
+    iIntros {v} "?"; by iExists L, Lv, _.
   Qed.
 End auth.
diff --git a/program_logic/ectx_weakestpre.v b/program_logic/ectx_lifting.v
similarity index 100%
rename from program_logic/ectx_weakestpre.v
rename to program_logic/ectx_lifting.v
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 1e978fcd7d313e614be0c4aa1523a822a01c709c..e5898f1f86c69a87d241eadbf7aa88b5f2a01481 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre viewshifts.
-From iris.proofmode Require Import weakestpre.
+From iris.proofmode Require Import weakestpre invariants.
 
 Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
     (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ :=
@@ -62,9 +62,9 @@ Lemma ht_vs E P P' Φ Φ' e :
   ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ ∀ v, Φ' v ={E}=> Φ v)
   ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
-  iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iPvs "Hvs" "HP" as "HP".
+  iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iPvs ("Hvs" with "HP") as "HP".
   iApply wp_pvs; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
-  iIntros {v} "Hv". by iApply "HΦ" "!".
+  iIntros {v} "Hv". by iApply ("HΦ" with "!").
 Qed.
 
 Lemma ht_atomic E1 E2 P P' Φ Φ' e :
@@ -73,9 +73,9 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
   ⊢ {{ P }} e @ E1 {{ Φ }}.
 Proof.
   iIntros {??} "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto.
-  iPvs "Hvs" "HP" as "HP"; first set_solver. iPvsIntro.
+  iPvs ("Hvs" with "HP") as "HP"; first set_solver. iPvsIntro.
   iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
-  iIntros {v} "Hv". by iApply "HΦ" "!".
+  iIntros {v} "Hv". by iApply ("HΦ" with "!").
 Qed.
 
 Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
@@ -84,7 +84,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
 Proof.
   iIntros "(#Hwpe&#HwpK) ! HP". iApply wp_bind.
   iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|].
-  iIntros {v} "Hv". by iApply "HwpK" "!".
+  iIntros {v} "Hv". by iApply ("HwpK" with "!").
 Qed.
 
 Lemma ht_mask_weaken E1 E2 P Φ e :
@@ -110,9 +110,8 @@ Proof.
   iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]".
   iApply (wp_frame_step_l E E1 E2); try done.
   iSplitL "HR"; [|by iApply "Hwp"].
-  iPvs "Hvs1" "HR"; first by set_solver.
-  iPvsIntro. iNext.
-  by iPvs "Hvs2" "Hvs1"; first by set_solver.
+  iPvs ("Hvs1" with "HR"); first by set_solver.
+  iPvsIntro. iNext. by iApply "Hvs2".
 Qed.
 
 Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
@@ -146,7 +145,6 @@ Lemma ht_inv N E P Φ R e :
   (inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ v, ▷ R ★ Φ v }})
     ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
-  iIntros {??} "[#? #Hwp] ! HP". eapply wp_inv; eauto.
-  iIntros "HR". iApply "Hwp". by iSplitL "HR".
+  iIntros {??} "[#? #Hwp] ! HP". iInv N as "HR". iApply "Hwp". by iSplitL "HR".
 Qed.
 End hoare.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 99ceeee64e6e168fa673d5a7e9bb52c7dc1d4b97..e64ef99d4bf7b948c77b5f7a4acb2525d78279b6 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -31,13 +31,13 @@ Lemma ht_lift_step E1 E2
 Proof.
   iIntros {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP".
   iApply (wp_lift_step E1 E2 φ _ e1 σ1); auto.
-  iPvs "Hvs" "HP" as "[Hσ HP]"; first set_solver.
+  iPvs ("Hvs" with "HP") as "[Hσ HP]"; first set_solver.
   iPvsIntro. iNext. iSplitL "Hσ"; [done|iIntros {e2 σ2 ef} "[#Hφ Hown]"].
-  iSpecialize "HΦ" {e2 σ2 ef} "! -". by iFrame "Hφ HP Hown".
+  iSpecialize ("HΦ" $! e2 σ2 ef with "! -"). by iFrame "Hφ HP Hown".
   iPvs "HΦ" as "[H1 H2]"; first by set_solver.
   iPvsIntro. iSplitL "H1".
-  - by iApply "He2" "!".
-  - destruct ef as [e|]; last done. by iApply "Hef" {_ _ (Some e)} "!".
+  - by iApply ("He2" with "!").
+  - destruct ef as [e|]; last done. by iApply ("Hef" $! _ _ (Some e) with "!").
 Qed.
 
 Lemma ht_lift_atomic_step
@@ -57,8 +57,8 @@ Proof.
   repeat iSplit.
   - by iApply vs_reflexive.
   - iIntros {e2 σ2 ef} "! (#Hφ&Hown&HP)"; iPvsIntro.
-    iSplitL "Hown". by iSplit. iSplit. by iPure "Hφ" as [_ ?]. done.
-  - iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iPure "Hφ" as [[v2 <-%of_to_val] ?].
+    iSplitL "Hown". by iSplit. iSplit. by iDestruct "Hφ" as %[_ ?]. done.
+  - iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?].
     iApply wp_value'. iExists σ2, ef. by iSplit.
   - done.
 Qed.
@@ -74,8 +74,9 @@ Proof.
   iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP".
   iApply (wp_lift_pure_step E φ _ e1); auto.
   iNext; iIntros {e2 ef Hφ}. iDestruct "HP" as "[HP HP']"; iSplitL "HP".
-  - iApply "He2" "!"; by iSplit.
-  - destruct ef as [e|]; last done. iApply "Hef" {_ (Some e)} "!"; by iSplit.
+  - iApply ("He2" with "!"); by iSplit.
+  - destruct ef as [e|]; last done.
+    iApply ("Hef" $! _ (Some e) with "!"); by iSplit.
 Qed.
 
 Lemma ht_lift_pure_det_step
@@ -89,8 +90,8 @@ Proof.
   iIntros {? Hsafe Hdet} "[#He2 #Hef]".
   iApply (ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
   iSplit; iIntros {e2' ef'}.
-  - iIntros "! [#He ?]"; iPure "He" as [-> ->]. by iApply "He2".
+  - iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "He2".
   - destruct ef' as [e'|]; last done.
-    iIntros "! [#He ?]"; iPure "He" as [-> ->]. by iApply "Hef" "!".
+    iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply ("Hef" with "!").
 Qed.
 End lifting.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index da98cfd995fe82414a8a5eb9906f680ac3d61bd7..3fb1ae7061ffa59f14391bf321bab8bc4c240188 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -1,11 +1,7 @@
-From iris.algebra Require Export base.
 From iris.program_logic Require Import ownership.
-From iris.program_logic Require Export namespaces pviewshifts weakestpre.
+From iris.program_logic Require Export namespaces.
+From iris.proofmode Require Import pviewshifts.
 Import uPred.
-Local Hint Extern 100 (@eq coPset _ _) => set_solver.
-Local Hint Extern 100 (@subseteq coPset _ _) => set_solver.
-Local Hint Extern 100 (_ ∉ _) => set_solver.
-Local Hint Extern 99 ({[ _ ]} ⊆ _) => apply elem_of_subseteq_singleton.
 
 (** Derived forms and lemmas about them. *)
 Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
@@ -29,72 +25,22 @@ Proof. rewrite /inv; apply _. Qed.
 Lemma always_inv N P : □ inv N P ⊣⊢ inv N P.
 Proof. by rewrite always_always. Qed.
 
-(** Invariants can be opened around any frame-shifting assertion. *)
-Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ R :
-  fsaV → nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a)) →
-  R ⊢ fsa E Ψ.
-Proof.
-  intros ? HN Hinv Hinner.
-  rewrite -[R](idemp (∧)%I) {1}Hinv Hinner =>{Hinv Hinner R}.
-  rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i.
-  rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
-  rewrite -(fsa_open_close E (E ∖ {[encode i]})) //; last by set_solver+.
-  (* Add this to the local context, so that set_solver finds it. *)
-  assert ({[encode i]} ⊆ nclose N) by eauto.
-  rewrite (always_sep_dup (ownI _ _)).
-  rewrite {1}pvs_openI !pvs_frame_r.
-  apply pvs_mask_frame_mono; [set_solver..|].
-  rewrite (comm _ (â–·_)%I) -assoc wand_elim_r fsa_frame_l.
-  apply fsa_mask_frame_mono; [set_solver..|]. intros a.
-  rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
-  apply pvs_mask_frame'; set_solver.
-Qed.
-Lemma inv_fsa_timeless {A} (fsa : FSA Λ Σ A)
-    `{!FrameShiftAssertion fsaV fsa} E N P `{!TimelessP P} Ψ R :
-  fsaV → nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (P -★ fsa (E ∖ nclose N) (λ a, P ★ Ψ a)) →
-  R ⊢ fsa E Ψ.
-Proof.
-  intros ??? HR. eapply inv_fsa, wand_intro_l; eauto.
-  trans (|={E ∖ N}=> P ★ R)%I; first by rewrite pvs_timeless pvs_frame_r.
-  apply (fsa_strip_pvs _). rewrite HR wand_elim_r.
-  apply: fsa_mono=> v. by rewrite -later_intro.
-Qed.
-
-(* Derive the concrete forms for pvs and wp, because they are useful. *)
-
-Lemma pvs_inv E N P Q R :
-  nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (▷ P -★ |={E ∖ nclose N}=> (▷ P ★ Q)) →
-  R ⊢ (|={E}=> Q).
-Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
-Lemma pvs_inv_timeless E N P `{!TimelessP P} Q R :
-  nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (P -★ |={E ∖ nclose N}=> (P ★ Q)) →
-  R ⊢ (|={E}=> Q).
-Proof. intros. by apply: (inv_fsa_timeless pvs_fsa). Qed.
-
-Lemma wp_inv E e N P Φ R :
-  atomic e → nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (▷ P -★ WP e @ E ∖ nclose N {{ v, ▷ P ★ Φ v }}) →
-  R ⊢ WP e @ E {{ Φ }}.
-Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
-Lemma wp_inv_timeless E e N P `{!TimelessP P} Φ R :
-  atomic e → nclose N ⊆ E →
-  R ⊢ inv N P →
-  R ⊢ (P -★ WP e @ E ∖ nclose N {{ v, P ★ Φ v }}) →
-  R ⊢ WP e @ E {{ Φ }}.
-Proof. intros. by apply: (inv_fsa_timeless (wp_fsa e)). Qed.
-
 Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ⊢ |={E}=> inv N P.
 Proof.
   intros. rewrite -(pvs_mask_weaken N) //.
   by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
 Qed.
+
+(** Invariants can be opened around any frame-shifting assertion. *)
+Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ :
+  fsaV → nclose N ⊆ E →
+  (inv N P ★ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a))) ⊢ fsa E Ψ.
+Proof.
+  iIntros {??} "[#Hinv HΨ]"; rewrite /inv; iDestruct "Hinv" as {i} "[% Hi]".
+  iApply (fsa_open_close E (E ∖ {[encode i]})); auto; first by set_solver.
+  iPvs (pvs_openI' _ _ with "Hi") as "HP"; [set_solver..|iPvsIntro].
+  iApply (fsa_mask_weaken _ (E ∖ N)); first set_solver.
+  iApply fsa_wand_r; iSplitL; [by iApply "HΨ"|iIntros {v} "[HP HΨ]"].
+  iPvs (pvs_closeI' _ _ P with "[HP]"); [auto|by iSplit|set_solver|done].
+Qed.
 End inv.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index cd2ee4887ec56bcc3bfa49a88b5286945ef374c1..96dfa57f560d05f4aaa62ebd4fdb683f781dba27 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -174,6 +174,10 @@ Proof.
   rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last set_solver.
   by rewrite {2}HEE -!union_difference_L.
 Qed.
+Lemma pvs_openI' E i P : i ∈ E → ownI i P ⊢ (|={E, E ∖ {[i]}}=> ▷ P).
+Proof. intros. etrans. apply pvs_openI. apply pvs_mask_frame'; set_solver. Qed.
+Lemma pvs_closeI' E i P : i ∈ E → (ownI i P ∧ ▷ P) ⊢ (|={E ∖ {[i]}, E}=> True).
+Proof. intros. etrans. apply pvs_closeI. apply pvs_mask_frame'; set_solver. Qed.
 
 Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
   E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
@@ -217,6 +221,7 @@ Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
 Section fsa.
 Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
 Implicit Types Φ Ψ : A → iProp Λ Σ.
+Import uPred.
 
 Lemma fsa_mono E Φ Ψ : (∀ a, Φ a ⊢ Ψ a) → fsa E Φ ⊢ fsa E Ψ.
 Proof. apply fsa_mask_frame_mono; auto. Qed.
@@ -231,8 +236,20 @@ Proof.
 Qed.
 Lemma fsa_pvs_fsa E Φ : (|={E}=> fsa E Φ) ⊣⊢ fsa E Φ.
 Proof. apply (anti_symm (⊢)); [by apply fsa_strip_pvs|apply pvs_intro]. Qed.
+Lemma pvs_fsa_fsa E Φ : fsa E (λ a, |={E}=> Φ a) ⊣⊢ fsa E Φ.
+Proof.
+  apply (anti_symm (⊢)); [|apply fsa_mono=> a; apply pvs_intro].
+  by rewrite (pvs_intro E (fsa E _)) fsa_trans3.
+Qed.
 Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ⊢ (|={E}=> Ψ a)) → fsa E Φ ⊢ fsa E Ψ.
 Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
+Lemma fsa_wand_l E Φ Ψ : ((∀ a, Φ a -★ Ψ a) ★ fsa E Φ) ⊢ (fsa E Ψ).
+Proof.
+  rewrite fsa_frame_l. apply fsa_mono=> a.
+  by rewrite (forall_elim a) wand_elim_l.
+Qed.
+Lemma fsa_wand_r E Φ Ψ : (fsa E Φ ★ ∀ a, Φ a -★ Ψ a) ⊢ (fsa E Ψ).
+Proof. by rewrite (comm _ (fsa _ _)) fsa_wand_l. Qed.
 End fsa.
 
 Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, (|={E}=> Φ ())%I.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index dfe31b9918245abcd5b5eaf23cdf174b6e97fbda..18fd96dac13cbfa5615b4c89418bf496f705024a 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export sts upred_tactics.
 From iris.program_logic Require Export invariants ghost_ownership.
+From iris.proofmode Require Import invariants ghost_ownership.
 Import uPred.
 
 (** The CMRA we need. *)
@@ -64,7 +65,7 @@ Section sts.
   Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
     T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 →
     sts_ownS γ S1 T1 ⊢ (|={E}=> sts_ownS γ S2 T2).
-  Proof. intros ? ? ?. by apply own_update, sts_update_frag. Qed.
+  Proof. intros ???. by apply own_update, sts_update_frag. Qed.
 
   Lemma sts_own_weaken E γ s S T1 T2 :
     T2 ⊆ T1 → s ∈ S → sts.closed S T2 →
@@ -80,86 +81,46 @@ Section sts.
     nclose N ⊆ E →
     ▷ φ s ⊢ (|={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
   Proof.
-    intros HN. eapply sep_elim_True_r.
-    { apply (own_alloc (sts_auth s (⊤ ∖ sts.tok s)) E).
-      apply sts_auth_valid; set_solver. }
-    rewrite pvs_frame_l. apply pvs_strip_pvs.
-    rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
-    trans (▷ sts_inv γ φ ★ sts_own γ s (⊤ ∖ sts.tok s))%I.
-    { rewrite /sts_inv -(exist_intro s) later_sep.
-      ecancel [▷ φ _]%I.
-      by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
-    rewrite (inv_alloc N E) // /sts_ctx pvs_frame_r.
-    by rewrite always_and_sep_l.
-  Qed.
-
-  Lemma sts_opened E γ S T :
-    (▷ sts_inv γ φ ★ sts_ownS γ S T)
-    ⊢ (|={E}=> ∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)).
-  Proof.
-    rewrite /sts_inv later_exist sep_exist_r. apply exist_elim=>s.
-    rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
-    rewrite -(exist_intro s). ecancel [▷ φ _]%I.
-    rewrite -own_op own_valid_l discrete_valid.
-    apply const_elim_sep_l=> Hvalid.
-    assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
-    rewrite const_equiv // left_id sts_op_auth_frag //.
-    by assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
-  Qed.
-
-  Lemma sts_closing E γ s T s' T' :
-    sts.steps (s, T) (s', T') →
-    (▷ φ s' ★ own γ (sts_auth s T)) ⊢ (|={E}=> ▷ sts_inv γ φ ★ sts_own γ s' T').
-  Proof.
-    intros Hstep. rewrite /sts_inv -(exist_intro s') later_sep.
-    (* TODO it would be really nice to use cancel here *)
-    rewrite [(_ ★ ▷ φ _)%I]comm -assoc.
-    rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
-    rewrite own_valid_l discrete_valid. apply const_elim_sep_l=>Hval.
-    trans (|={E}=> own γ (sts_auth s' T'))%I.
-    { by apply own_update, sts_update_auth. }
-    by rewrite -own_op sts_op_auth_frag_up.
+    iIntros {?} "Hφ". rewrite /sts_ctx /sts_own.
+    iPvs (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as {γ} "Hγ".
+    { apply sts_auth_valid; set_solver. }
+    iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
+    iPvs (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
+    iNext. iExists s. by iFrame "Hφ".
   Qed.
 
   Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
 
-  Lemma sts_fsaS E N P (Ψ : V → iPropG Λ Σ) γ S T :
+  Lemma sts_fsaS E N (Ψ : V → iPropG Λ Σ) γ S T :
     fsaV → nclose N ⊆ E →
-    P ⊢ sts_ctx γ N φ →
-    P ⊢ (sts_ownS γ S T ★ ∀ s,
-          ■ (s ∈ S) ★ ▷ φ s -★
-          fsa (E ∖ nclose N) (λ x, ∃ s' T',
-            ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★
-            (sts_own γ s' T' -★ Ψ x))) →
-    P ⊢ fsa E Ψ.
+    (sts_ctx γ N φ ★ sts_ownS γ S T ★ ∀ s,
+      ■ (s ∈ S) ★ ▷ φ s -★
+      fsa (E ∖ nclose N) (λ x, ∃ s' T',
+        ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★ (sts_own γ s' T' -★ Ψ x)))
+    ⊢ fsa E Ψ.
   Proof.
-    rewrite /sts_ctx=>? HN Hinv Hinner.
-    eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
-    apply wand_intro_l. rewrite assoc.
-    rewrite (sts_opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
-    apply (fsa_strip_pvs fsa). apply exist_elim=>s.
-    rewrite (forall_elim s). rewrite [(▷_ ★ _)%I]comm.
-    eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
-    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc. done. }
-    rewrite fsa_frame_l.
-    apply (fsa_mono_pvs fsa)=> x.
-    rewrite sep_exist_l; apply exist_elim=> s'.
-    rewrite sep_exist_l; apply exist_elim=>T'.
-    rewrite comm -!assoc. apply const_elim_sep_l=>-Hstep.
-    rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc.
-    rewrite (sts_closing (E ∖ N)) //; [].
-    rewrite pvs_frame_l. apply pvs_mono.
-    by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
+    iIntros {??} "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
+    iInv N as {s} "[Hγ Hφ]"; iTimeless "Hγ".
+    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ !") as %Hvalid.
+    assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
+    assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
+    iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ".
+    iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
+    { iApply "HΨ"; by iSplit. }
+    iIntros {a} "H"; iDestruct "H" as {s' T'} "(% & Hφ & HΨ)".
+    iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
+    iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]".
+    iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ".
+    iNext; iExists s'; by iFrame "Hφ".
   Qed.
 
-  Lemma sts_fsa E N P (Ψ : V → iPropG Λ Σ) γ s0 T :
+  Lemma sts_fsa E N (Ψ : V → iPropG Λ Σ) γ s0 T :
     fsaV → nclose N ⊆ E →
-    P ⊢ sts_ctx γ N φ →
-    P ⊢ (sts_own γ s0 T ★ ∀ s,
-          ■ (s ∈ sts.up s0 T) ★ ▷ φ s -★
-          fsa (E ∖ nclose N) (λ x, ∃ s' T',
-            ■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ★
-            (sts_own γ s' T' -★ Ψ x))) →
-    P ⊢ fsa E Ψ.
+    (sts_ctx γ N φ ★ sts_own γ s0 T ★ ∀ s,
+      ■ (s ∈ sts.up s0 T) ★ ▷ φ s -★
+      fsa (E ∖ nclose N) (λ x, ∃ s' T',
+        ■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ★
+        (sts_own γ s' T' -★ Ψ x)))
+    ⊢ fsa E Ψ.
   Proof. by apply sts_fsaS. Qed.
 End sts.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index ba657409b7ff81dbdfdd28ec29490df72581cd39..5e2dbdeda85a33d37821417e326bf2cb11276e8c 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import ownership.
 From iris.program_logic Require Export pviewshifts invariants ghost_ownership.
-From iris.proofmode Require Import pviewshifts.
+From iris.proofmode Require Import pviewshifts invariants.
 Import uPred.
 
 Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
@@ -65,7 +65,7 @@ Lemma vs_transitive E1 E2 E3 P Q R :
   E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R)) ⊢ (P ={E1,E3}=> R).
 Proof.
   iIntros {?} "#[HvsP HvsQ] ! HP".
-  iPvs "HvsP" "! HP" as "HQ"; first done. by iApply "HvsQ" "!".
+  iPvs ("HvsP" with "! HP") as "HQ"; first done. by iApply ("HvsQ" with "!").
 Qed.
 
 Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊢ (P ={E}=> R).
@@ -94,8 +94,8 @@ Proof. intros; apply vs_mask_frame; set_solver. Qed.
 Lemma vs_inv N E P Q R :
   nclose N ⊆ E → (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q).
 Proof.
-  iIntros {?} "#[? Hvs] ! HP". eapply pvs_inv; eauto.
-  iIntros "HR". iApply "Hvs" "!". by iSplitL "HR".
+  iIntros {?} "#[? Hvs] ! HP". iInv N as "HR".
+  iApply ("Hvs" with "!"). by iSplitL "HR".
 Qed.
 
 Lemma vs_alloc N P : â–· P ={N}=> inv N P.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 9b3c212fc4361d93a6ce32631fdc1821e9ef7030..17a8778f9650d440b73c7453f224fcd48aaf0586 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export upred.
 From iris.algebra Require Import upred_big_op upred_tactics.
 From iris.proofmode Require Export environments.
-From iris.prelude Require Import stringmap.
+From iris.prelude Require Import stringmap hlist.
 Import uPred.
 
 Local Notation "Γ !! j" := (env_lookup j Γ).
@@ -26,6 +26,12 @@ Record envs_wf {M} (Δ : envs M) := {
 
 Coercion of_envs {M} (Δ : envs M) : uPred M :=
   (■ envs_wf Δ ★ □ Π∧ env_persistent Δ ★ Π★ env_spatial Δ)%I.
+Instance: Params (@of_envs) 1.
+
+Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
+  env_persistent_Forall2 : env_Forall2 R (env_persistent Δ1) (env_persistent Δ2);
+  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
+}.
 
 Instance envs_dom {M} : Dom (envs M) stringset := λ Δ,
   dom stringset (env_persistent Δ) ∪ dom stringset (env_spatial Δ).
@@ -252,6 +258,39 @@ Lemma envs_persistent_persistent Δ : envs_persistent Δ = true → PersistentP
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
 Hint Immediate envs_persistent_persistent : typeclass_instances.
 
+Global Instance envs_Forall2_refl (R : relation (uPred M)) :
+  Reflexive R → Reflexive (envs_Forall2 R).
+Proof. by constructor. Qed.
+Global Instance envs_Forall2_sym (R : relation (uPred M)) :
+  Symmetric R → Symmetric (envs_Forall2 R).
+Proof. intros ??? [??]; by constructor. Qed.
+Global Instance envs_Forall2_trans (R : relation (uPred M)) :
+  Transitive R → Transitive (envs_Forall2 R).
+Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
+Global Instance envs_Forall2_antisymm (R R' : relation (uPred M)) :
+  AntiSymm R R' → AntiSymm (envs_Forall2 R) (envs_Forall2 R').
+Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
+Lemma envs_Forall2_impl (R R' : relation (uPred M)) Δ1 Δ2 :
+  envs_Forall2 R Δ1 Δ2 → (∀ P Q, R P Q → R' P Q) → envs_Forall2 R' Δ1 Δ2.
+Proof. intros [??] ?; constructor; eauto using env_Forall2_impl. Qed.
+
+Global Instance of_envs_mono : Proper (envs_Forall2 (⊢) ==> (⊢)) (@of_envs M).
+Proof.
+  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; unfold of_envs; simpl in *.
+  apply const_elim_sep_l=>Hwf. apply sep_intro_True_l.
+  - destruct Hwf; apply const_intro; constructor;
+      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
+  - by repeat f_equiv.
+Qed.
+Global Instance of_envs_proper : Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs M).
+Proof.
+  intros Δ1 Δ2 ?; apply (anti_symm (⊢)); apply of_envs_mono;
+    eapply envs_Forall2_impl; [| |symmetry|]; eauto using equiv_entails.
+Qed.
+Global Instance Envs_mono (R : relation (uPred M)) :
+  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
+Proof. by constructor. Qed.
+
 (** * Adequacy *)
 Lemma tac_adequate P : Envs Enil Enil ⊢ P → True ⊢ P.
 Proof.
@@ -287,25 +326,12 @@ Lemma tac_clear_spatial Δ Δ' Q :
   envs_clear_spatial Δ = Δ' → Δ' ⊢ Q → Δ ⊢ Q.
 Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
 
-Lemma tac_duplicate Δ Δ' i p j P Q :
-  envs_lookup i Δ = Some (p, P) →
-  p = true →
-  envs_simple_replace i true (Esnoc (Esnoc Enil i P) j P) Δ = Some Δ' →
-  Δ' ⊢ Q → Δ ⊢ Q.
-Proof.
-  intros ? -> ??. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id idemp wand_elim_r.
-Qed.
-
 (** * False *)
 Lemma tac_ex_falso Δ Q : Δ ⊢ False → Δ ⊢ Q.
 Proof. by rewrite -(False_elim Q). Qed.
 
 (** * Pure *)
-Lemma tac_pure_intro Δ (φ : Prop) : φ → Δ ⊢ ■ φ.
-Proof. apply const_intro. Qed.
-
-Class ToPure (P : uPred M) (φ : Prop) := to_pure : P ⊢ ■ φ.
+Class ToPure (P : uPred M) (φ : Prop) := to_pure : P ⊣⊢ ■ φ.
 Arguments to_pure : clear implicits.
 Global Instance to_pure_const φ : ToPure (■ φ) φ.
 Proof. done. Qed.
@@ -315,6 +341,9 @@ Proof. intros; red. by rewrite timeless_eq. Qed.
 Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure (✓ a) (✓ a).
 Proof. intros; red. by rewrite discrete_valid. Qed.
 
+Lemma tac_pure_intro Δ Q (φ : Prop) : ToPure Q φ → φ → Δ ⊢ Q.
+Proof. intros ->. apply const_intro. Qed.
+
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') → ToPure P φ →
   (φ → Δ' ⊢ Q) → Δ ⊢ Q.
@@ -560,12 +589,35 @@ Proof.
   by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
 Qed.
 
-Lemma tac_pose_proof Δ Δ' j P Q :
-  True ⊢ P → envs_app true (Esnoc Enil j P) Δ = Some Δ' →
+(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
+not as [H : True -★ Q]. The class [ToPosedProof] is used to strip off the
+[True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
+make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *)
+Class ToPosedProof (P1 P2 R : uPred M) := to_pose_proof : P1 ⊢ P2 → True ⊢ R.
+Arguments to_pose_proof : clear implicits.
+Instance to_posed_proof_True P : ToPosedProof True P P.
+Proof. by rewrite /ToPosedProof. Qed.
+Global Instance to_posed_proof_wand P Q : ToPosedProof P Q (P -★ Q).
+Proof. rewrite /ToPosedProof. apply entails_wand. Qed.
+
+Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
+  P1 ⊢ P2 → ToPosedProof P1 P2 R → envs_app true (Esnoc Enil j R) Δ = Some Δ' →
   Δ' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros HP ? <-. rewrite envs_app_sound //; simpl.
-  by rewrite -HP left_id always_const wand_True.
+  intros HP ?? <-. rewrite envs_app_sound //; simpl.
+  by rewrite right_id -(to_pose_proof P1 P2 R) // always_const wand_True.
+Qed.
+
+Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
+  envs_lookup_delete i Δ = Some (p, P, Δ') →
+  envs_app p (Esnoc Enil j P) (if p then Δ else Δ') = Some Δ'' →
+  Δ'' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
+  - rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
+    by rewrite right_id wand_elim_r.
+  - rewrite envs_lookup_sound // envs_app_sound //; simpl.
+    by rewrite right_id wand_elim_r.
 Qed.
 
 Lemma tac_apply Δ Δ' i p R P1 P2 :
@@ -718,25 +770,25 @@ Class Frame (R P : uPred M) (mQ : option (uPred M)) :=
   frame : (R ★ from_option True mQ) ⊢ P.
 Arguments frame : clear implicits.
 
-Instance frame_here R : Frame R R None | 1.
+Global Instance frame_here R : Frame R R None.
 Proof. by rewrite /Frame right_id. Qed.
-Instance frame_sep_l R P1 P2 mQ :
+Global Instance frame_sep_l R P1 P2 mQ :
   Frame R P1 mQ →
-  Frame R (P1 ★ P2) (Some $ if mQ is Some Q then Q ★ P2 else P2)%I.
+  Frame R (P1 ★ P2) (Some $ if mQ is Some Q then Q ★ P2 else P2)%I | 9.
 Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
-Instance frame_sep_r R P1 P2 mQ :
+Global Instance frame_sep_r R P1 P2 mQ :
   Frame R P2 mQ →
-  Frame R (P1 ★ P2) (Some $ if mQ is Some Q then P1 ★ Q else P1)%I.
+  Frame R (P1 ★ P2) (Some $ if mQ is Some Q then P1 ★ Q else P1)%I | 10.
 Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
-Instance frame_and_l R P1 P2 mQ :
+Global Instance frame_and_l R P1 P2 mQ :
   Frame R P1 mQ →
-  Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then Q ∧ P2 else P2)%I.
+  Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then Q ∧ P2 else P2)%I | 9.
 Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
-Instance frame_and_r R P1 P2 mQ :
+Global Instance frame_and_r R P1 P2 mQ :
   Frame R P2 mQ →
-  Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then P1 ∧ Q else P1)%I.
+  Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then P1 ∧ Q else P1)%I | 10.
 Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
-Instance frame_or R P1 P2 mQ1 mQ2 :
+Global Instance frame_or R P1 P2 mQ1 mQ2 :
   Frame R P1 mQ1 → Frame R P2 mQ2 →
   Frame R (P1 ∨ P2) (match mQ1, mQ2 with
                      | Some Q1, Some Q2 => Some (Q1 ∨ Q2)%I | _, _ => None
@@ -746,17 +798,17 @@ Proof.
   destruct mQ1 as [Q1|], mQ2 as [Q2|]; simpl; auto with I.
   by rewrite -sep_or_l.
 Qed.
-Instance frame_later R P mQ :
+Global Instance frame_later R P mQ :
   Frame R P mQ → Frame R (▷ P) (if mQ is Some Q then Some (▷ Q) else None)%I.
 Proof.
   rewrite /Frame=><-.
   by destruct mQ; rewrite /= later_sep -(later_intro R) ?later_True.
 Qed.
-Instance frame_exist {A} R (Φ : A → uPred M) mΨ :
+Global Instance frame_exist {A} R (Φ : A → uPred M) mΨ :
   (∀ a, Frame R (Φ a) (mΨ a)) →
   Frame R (∃ x, Φ x) (Some (∃ x, if mΨ x is Some Q then Q else True))%I.
 Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
-Instance frame_forall {A} R (Φ : A → uPred M) mΨ :
+Global Instance frame_forall {A} R (Φ : A → uPred M) mΨ :
   (∀ a, Frame R (Φ a) (mΨ a)) →
   Frame R (∀ x, Φ x) (Some (∀ x, if mΨ x is Some Q then Q else True))%I.
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
@@ -815,13 +867,26 @@ Qed.
 Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ ⊢ (∀ a, Φ a).
 Proof. apply forall_intro. Qed.
 
-Lemma tac_forall_specialize {A} Δ Δ' i p (Φ : A → uPred M) Q a :
-  envs_lookup i Δ = Some (p, ∀ a, Φ a)%I →
-  envs_simple_replace i p (Esnoc Enil i (Φ a)) Δ = Some Δ' →
+Class ForallSpecialize {As} (xs : hlist As)
+    (P : uPred M) (Φ : himpl As (uPred M)) :=
+  forall_specialize : P ⊢ happly Φ xs.
+Arguments forall_specialize {_} _ _ _ {_}.
+
+Global Instance forall_specialize_nil P : ForallSpecialize hnil P P | 100.
+Proof. done. Qed.
+Global Instance forall_specialize_cons A As x xs Φ (Ψ : A → himpl As (uPred M)) :
+  (∀ x, ForallSpecialize xs (Φ x) (Ψ x)) →
+  ForallSpecialize (hcons x xs) (∀ x : A, Φ x) Ψ.
+Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.
+
+Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
+  envs_lookup i Δ = Some (p, P) → ForallSpecialize xs P Φ →
+  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_elim a) wand_elim_r.
+  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.
 Qed.
 
 Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
@@ -846,8 +911,8 @@ Global Instance exist_destruct_exist {A} (Φ : A → uPred M) :
   ExistDestruct (∃ a, Φ a) Φ.
 Proof. done. Qed.
 Global Instance exist_destruct_later {A} P (Φ : A → uPred M) :
-  Inhabited A → ExistDestruct P Φ → ExistDestruct (▷ P) (λ a, ▷ (Φ a))%I.
-Proof. rewrite /ExistDestruct=> ? ->. by rewrite later_exist. Qed.
+  ExistDestruct P Φ → Inhabited A → ExistDestruct (▷ P) (λ a, ▷ (Φ a))%I.
+Proof. rewrite /ExistDestruct=> HP ?. by rewrite HP later_exist. Qed.
 
 Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q :
   envs_lookup i Δ = Some (p, P)%I → ExistDestruct P Φ →
@@ -867,18 +932,5 @@ Proof.
 Qed.
 End tactics.
 
-(** Make sure we can frame in the presence of evars without making Coq loop due
-to it applying these rules too eager.
-
-Note: that [Hint Mode Frame - + + - : typeclass_instances] would disable framing
-with evars entirely.
-Note: we give presence to framing on the left. *)
-Hint Extern 0 (Frame _ ?R _) => class_apply @frame_here : typeclass_instances.
-Hint Extern 9 (Frame _ (_ ★ _) _) => class_apply @frame_sep_l : typeclass_instances.
-Hint Extern 10 (Frame _ (_ ★ _) _) => class_apply @frame_sep_r : typeclass_instances.
-Hint Extern 9 (Frame _ (_ ∧ _) _) => class_apply @frame_and_l : typeclass_instances.
-Hint Extern 10 (Frame _ (_ ∧ _) _) => class_apply @frame_and_r : typeclass_instances.
-Hint Extern 10 (Frame _ (_ ∨ _) _) => class_apply @frame_or : typeclass_instances.
-Hint Extern 10 (Frame _ (â–· _) _) => class_apply @frame_later : typeclass_instances.
-Hint Extern 10 (Frame _ (∃ _, _) _) => class_apply @frame_exist : typeclass_instances.
-Hint Extern 10 (Frame _ (∀ _, _) _) => class_apply @frame_forall : typeclass_instances.
+Hint Extern 0 (ToPosedProof True _ _) =>
+  class_apply @to_posed_proof_True : typeclass_instances.
diff --git a/proofmode/environments.v b/proofmode/environments.v
index f513a6a2cec6f5cc0ac34bfd5688023e29fe0729..aa5cc9131755d50f531fcd9bca5ad95e15b1875b 100644
--- a/proofmode/environments.v
+++ b/proofmode/environments.v
@@ -7,6 +7,8 @@ Inductive env (A : Type) : Type :=
   | Esnoc : env A → string → A → env A.
 Arguments Enil {_}.
 Arguments Esnoc {_} _ _%string _.
+Instance: Params (@Enil) 1.
+Instance: Params (@Esnoc) 1.
 
 Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
 Local Notation "' ( x1 , x2 ) ← y ; z" :=
@@ -28,6 +30,7 @@ Inductive env_wf {A} : env A → Prop :=
 Fixpoint env_to_list {A} (E : env A) : list A :=
   match E with Enil => [] | Esnoc Γ _ x => x :: env_to_list Γ end.
 Coercion env_to_list : env >-> list.
+Instance: Params (@env_to_list) 1.
 
 Instance env_dom {A} : Dom (env A) stringset :=
   fix go Γ := let _ : Dom _ _ := @go in
@@ -201,6 +204,32 @@ Proof. intros. apply (env_split_go_wf Enil Γ Γ1 Γ2 js); eauto. Qed.
 Lemma env_split_perm Γ Γ1 Γ2 js : env_split js Γ = Some (Γ1,Γ2) → Γ ≡ₚ Γ1 ++ Γ2.
 Proof. apply env_split_go_perm. Qed.
 
+Global Instance env_Forall2_refl (P : relation A) :
+  Reflexive P → Reflexive (env_Forall2 P).
+Proof. intros ? Γ. induction Γ; constructor; auto. Qed.
+Global Instance env_Forall2_sym (P : relation A) :
+  Symmetric P → Symmetric (env_Forall2 P).
+Proof. induction 2; constructor; auto. Qed.
+Global Instance env_Forall2_trans (P : relation A) :
+  Transitive P → Transitive (env_Forall2 P).
+Proof.
+  intros ? Γ1 Γ2 Γ3 HΓ; revert Γ3.
+  induction HΓ; inversion_clear 1; constructor; eauto.
+Qed.
+Global Instance env_Forall2_antisymm (P Q : relation A) :
+  AntiSymm P Q → AntiSymm (env_Forall2 P) (env_Forall2 Q).
+Proof. induction 2; inversion_clear 1; constructor; auto. Qed.
+Lemma env_Forall2_impl {B} (P Q : A → B → Prop) Γ Σ :
+  env_Forall2 P Γ Σ → (∀ x y, P x y → Q x y) → env_Forall2 Q Γ Σ.
+Proof. induction 1; constructor; eauto. Qed.
+
+Global Instance Esnoc_proper (P : relation A) :
+  Proper (env_Forall2 P ==> (=) ==> P ==> env_Forall2 P) Esnoc.
+Proof. intros Γ1 Γ2 HΓ i ? <-; by constructor. Qed.
+Global Instance env_to_list_proper (P : relation A) :
+  Proper (env_Forall2 P ==> Forall2 P) env_to_list.
+Proof. induction 1; constructor; auto. Qed.
+
 Lemma env_Forall2_fresh {B} (P : A → B → Prop) Γ Σ i :
   env_Forall2 P Γ Σ → Γ !! i = None → Σ !! i = None.
 Proof. by induction 1; simplify. Qed.
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index cf5aa9e29688100a3d2dd69557495696ebeffe61..6595977c93d8767e440f14281550a01f2e9f526e 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -4,20 +4,23 @@ Inductive intro_pat :=
   | IName : string → intro_pat
   | IAnom : intro_pat
   | IAnomPure : intro_pat
-  | IClear : intro_pat
+  | IDrop : intro_pat
   | IFrame : intro_pat
   | IPersistent : intro_pat → intro_pat
   | IList : list (list intro_pat) → intro_pat
   | ISimpl : intro_pat
   | IAlways : intro_pat
-  | INext : intro_pat.
+  | INext : intro_pat
+  | IForall : intro_pat
+  | IAll : intro_pat
+  | IClear : list string → intro_pat.
 
 Module intro_pat.
 Inductive token :=
   | TName : string → token
   | TAnom : token
   | TAnomPure : token
-  | TClear : token
+  | TDrop : token
   | TFrame : token
   | TPersistent : token
   | TBar : token
@@ -28,7 +31,11 @@ Inductive token :=
   | TParenR : token
   | TSimpl : token
   | TAlways : token
-  | TNext : token.
+  | TNext : token
+  | TClearL : token
+  | TClearR : token
+  | TForall : token
+  | TAll : token.
 
 Fixpoint cons_name (kn : string) (k : list token) : list token :=
   match kn with "" => k | _ => TName (string_rev kn) :: k end.
@@ -38,7 +45,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String " " s => tokenize_go s (cons_name kn k) ""
   | String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
   | String "%" s => tokenize_go s (TAnomPure :: cons_name kn k) ""
-  | String "_" s => tokenize_go s (TClear :: cons_name kn k) ""
+  | String "_" s => tokenize_go s (TDrop :: cons_name kn k) ""
   | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
   | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
   | String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
@@ -49,7 +56,11 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "&" s => tokenize_go s (TAmp :: cons_name kn k) ""
   | String "!" s => tokenize_go s (TAlways :: cons_name kn k) ""
   | String ">" s => tokenize_go s (TNext :: cons_name kn k) ""
+  | String "{" s => tokenize_go s (TClearL :: cons_name kn k) ""
+  | String "}" s => tokenize_go s (TClearR :: cons_name kn k) ""
   | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
+  | String "*" (String "*" s) => tokenize_go s (TAll :: cons_name kn k) ""
+  | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
   | String a s => tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
@@ -60,19 +71,19 @@ Inductive stack_item :=
   | SList : stack_item
   | SConjList : stack_item
   | SBar : stack_item
-  | SAmp : stack_item.
+  | SAmp : stack_item
+  | SClear : stack_item.
 Notation stack := (list stack_item).
 
 Fixpoint close_list (k : stack)
     (ps : list intro_pat) (pss : list (list intro_pat)) : option stack :=
   match k with
-  | [] => None
   | SList :: k => Some (SPat (IList (ps :: pss)) :: k)
   | SPat pat :: k => close_list k (pat :: ps) pss
   | SPersistent :: k =>
      '(p,ps) ← maybe2 (::) ps; close_list k (IPersistent p :: ps) pss
   | SBar :: k => close_list k [] (ps :: pss)
-  | (SAmp | SConjList) :: _ => None
+  | _ => None
   end.
 
 Fixpoint big_conj (ps : list intro_pat) : intro_pat :=
@@ -86,7 +97,6 @@ Fixpoint big_conj (ps : list intro_pat) : intro_pat :=
 Fixpoint close_conj_list (k : stack)
     (cur : option intro_pat) (ps : list intro_pat) : option stack :=
   match k with
-  | [] => None
   | SConjList :: k =>
      ps ← match cur with
           | None => guard (ps = []); Some [] | Some p => Some (p :: ps)
@@ -95,7 +105,14 @@ Fixpoint close_conj_list (k : stack)
   | SPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
   | SPersistent :: k => p ← cur; close_conj_list k (Some (IPersistent p)) ps
   | SAmp :: k => p ← cur; close_conj_list k None (p :: ps)
-  | (SBar | SList) :: _ => None
+  | _ => None
+  end.
+
+Fixpoint close_clear (k : stack) (ss : list string) : option stack :=
+  match k with
+  | SPat (IName s) :: k => close_clear k (s :: ss)
+  | SClear :: k => Some (SPat (IClear (reverse ss)) :: k)
+  | _ => None
   end.
 
 Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
@@ -104,7 +121,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TName s :: ts => parse_go ts (SPat (IName s) :: k)
   | TAnom :: ts => parse_go ts (SPat IAnom :: k)
   | TAnomPure :: ts => parse_go ts (SPat IAnomPure :: k)
-  | TClear :: ts => parse_go ts (SPat IClear :: k)
+  | TDrop :: ts => parse_go ts (SPat IDrop :: k)
   | TFrame :: ts => parse_go ts (SPat IFrame :: k)
   | TPersistent :: ts => parse_go ts (SPersistent :: k)
   | TBracketL :: ts => parse_go ts (SList :: k)
@@ -116,6 +133,10 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
   | TAlways :: ts => parse_go ts (SPat IAlways :: k)
   | TNext :: ts => parse_go ts (SPat INext :: k)
+  | TAll :: ts => parse_go ts (SPat IAll :: k)
+  | TForall :: ts => parse_go ts (SPat IForall :: k)
+  | TClearL :: ts => parse_go ts (SClear :: k)
+  | TClearR :: ts => close_clear k [] ≫= parse_go ts
   end.
 Definition parse (s : string) : option (list intro_pat) :=
   match k ← parse_go (tokenize s) [SList]; close_list k [] [] with
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index d2161d80e68c22181c3fd6d77f2332c4df7ca698..9758f82bcd7742db832d361bd217cc4469deab40 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -14,7 +14,8 @@ Lemma tac_inv_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
   envs_app false (Esnoc Enil i (▷ P)) Δ = Some Δ' →
   Δ' ⊢ fsa (E ∖ nclose N) (λ a, ▷ P ★ Φ a) → Δ ⊢ Q.
 Proof.
-  intros ????? HΔ'. rewrite -(fsa_split Q). eapply (inv_fsa fsa); eauto.
+  intros ????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
+  rewrite // -always_and_sep_l. apply and_intro; first done.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
 Qed.
 
@@ -24,14 +25,16 @@ Lemma tac_inv_fsa_timeless {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   Δ' ⊢ fsa (E ∖ nclose N) (λ a, P ★ Φ a) → Δ ⊢ Q.
 Proof.
-  intros ?????? HΔ'. rewrite -(fsa_split Q).
-  eapply (inv_fsa_timeless fsa); eauto.
-  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
+  intros ?????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
+  rewrite // -always_and_sep_l. apply and_intro, wand_intro_l; first done.
+  trans (|={E ∖ N}=> P ★ Δ)%I; first by rewrite pvs_timeless pvs_frame_r.
+  apply (fsa_strip_pvs _).
+  rewrite envs_app_sound //; simpl. rewrite right_id HΔ' wand_elim_r.
+  apply: fsa_mono=> v. by rewrite -later_intro.
 Qed.
 End invariants.
 
-Tactic Notation "iInv" constr(N) "as" constr(pat) :=
-  let H := iFresh in
+Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
   eapply tac_inv_fsa with _ _ _ _ N H _ _;
     [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
@@ -39,10 +42,25 @@ Tactic Notation "iInv" constr(N) "as" constr(pat) :=
     |done || eauto with ndisj (* [eauto with ndisj] is slow *)
     |iAssumption || fail "iInv: invariant" N "not found"
     |env_cbv; reflexivity
-    |simpl (* get rid of FSAs *); iDestruct H as pat].
+    |simpl (* get rid of FSAs *)].
 
-Tactic Notation "iInv>" constr(N) "as" constr(pat) :=
-  let H := iFresh in
+Tactic Notation "iInv" constr(N) "as" constr(pat) :=
+  let H := iFresh in iInvCore N as H; last iDestruct H as pat.
+Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1) "}"
+    constr(pat) :=
+  let H := iFresh in iInvCore N as H; last iDestruct H as {x1} pat.
+Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) "}" constr(pat) :=
+  let H := iFresh in iInvCore N as H; last iDestruct H as {x1 x2} pat.
+Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
+  let H := iFresh in iInvCore N as H; last iDestruct H as {x1 x2 x3} pat.
+Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
+    constr(pat) :=
+  let H := iFresh in iInvCore N as H; last iDestruct H as {x1 x2 x3 x4} pat.
+
+Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
   eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
     [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
@@ -52,4 +70,20 @@ Tactic Notation "iInv>" constr(N) "as" constr(pat) :=
     |let P := match goal with |- TimelessP ?P => P end in
      apply _ || fail "iInv:" P "not timeless"
     |env_cbv; reflexivity
-    |simpl (* get rid of FSAs *); iDestruct H as pat].
+    |simpl (* get rid of FSAs *)].
+
+Tactic Notation "iInv>" constr(N) "as" constr(pat) :=
+  let H := iFresh in iInvCore> N as H; last iDestruct H as pat.
+Tactic Notation "iInv>" constr(N) "as" "{" simple_intropattern(x1) "}"
+    constr(pat) :=
+  let H := iFresh in iInvCore> N as H; last iDestruct H as {x1} pat.
+Tactic Notation "iInv>" constr(N) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) "}" constr(pat) :=
+  let H := iFresh in iInvCore> N as H; last iDestruct H as {x1 x2} pat.
+Tactic Notation "iInv>" constr(N) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
+  let H := iFresh in iInvCore> N as H; last iDestruct H as {x1 x2 x3} pat.
+Tactic Notation "iInv>" constr(N) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
+    constr(pat) :=
+  let H := iFresh in iInvCore> N as H; last iDestruct H as {x1 x2 x3 x4} pat.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index bc661a364963ed389c1640797628280a56465635..d5e8f86a8e79c604f0c6e78647182aafe0e4de8d 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -21,9 +21,9 @@ Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Λ Σ) :
 Proof.
   rewrite /ExistSplit=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
 Qed.
-Instance frame_pvs E1 E2 R P mQ :
+Global Instance frame_pvs E1 E2 R P mQ :
   Frame R P mQ →
-  Frame R (|={E1,E2}=> P) (Some (|={E1,E2}=> from_option True mQ))%I.
+  Frame R (|={E1,E2}=> P) (Some (|={E1,E2}=> if mQ is Some Q then Q else True))%I.
 Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
 Global Instance to_wand_pvs E1 E2 R P Q :
   ToWand R P Q → ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q).
@@ -32,12 +32,15 @@ Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
 Class FSASplit {A} (P : iProp Λ Σ) (E : coPset)
     (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A → iProp Λ Σ) := {
   fsa_split : fsa E Φ ⊢ P;
-  fsa_split_fsa :> FrameShiftAssertion fsaV fsa;
+  fsa_split_is_fsa :> FrameShiftAssertion fsaV fsa;
 }.
 Global Arguments fsa_split {_} _ _ _ _ _ {_}.
 Global Instance fsa_split_pvs E P :
   FSASplit (|={E}=> P)%I E pvs_fsa True (λ _, P).
 Proof. split. done. apply _. Qed.
+Global Instance fsa_split_fsa {A} (fsa : FSA Λ Σ A) E Φ :
+  FrameShiftAssertion fsaV fsa → FSASplit (fsa E Φ) E fsa fsaV Φ.
+Proof. done. Qed.
 
 Lemma tac_pvs_intro Δ E Q : Δ ⊢ Q → Δ ⊢ |={E}=> Q.
 Proof. intros ->. apply pvs_intro. Qed.
@@ -97,9 +100,6 @@ Proof.
 Qed.
 End pvs.
 
-Hint Extern 10 (Frame _ (|={_,_}=> _) _) =>
-  class_apply frame_pvs : typeclass_instances.
-
 Tactic Notation "iPvsIntro" := apply tac_pvs_intro.
 
 Tactic Notation "iPvsCore" constr(H) :=
@@ -118,89 +118,44 @@ Tactic Notation "iPvsCore" constr(H) :=
   end.
 
 Tactic Notation "iPvs" open_constr(H) :=
-  iPoseProof H as (fun H => iPvsCore H; last iDestruct H as "?").
+  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?").
 Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
-  iPoseProof H as (fun H => iPvsCore H; last iDestruct H as pat).
+  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1) "}"
     constr(pat) :=
-  iPoseProof H as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
+  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) "}" constr(pat) :=
-  iPoseProof H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 } pat).
+  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
-  iPoseProof H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
+  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
     constr(pat) :=
-  iPoseProof H as (fun H =>
+  iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) "}" constr(pat) :=
-  iPoseProof H as (fun H =>
+  iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
-  iPoseProof H as (fun H =>
+  iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
     constr(pat) :=
-  iPoseProof H as (fun H =>
+  iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
 Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
     simple_intropattern(x8) "}" constr(pat) :=
-  iPoseProof H as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
-
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) :=
-  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as "?").
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" constr(pat) :=
-  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) "}"
-    constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) "}"
-    constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
-    simple_intropattern(x7) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
-    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
-Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
-    simple_intropattern(x7) simple_intropattern(x8) "}" constr(pat) :=
-  iPoseProof lem Hs as (fun H =>
+  iDestructHelp H as (fun H =>
     iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
 
 Tactic Notation "iTimeless" constr(H) :=
@@ -228,7 +183,7 @@ Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
   let H := iFresh in
   let Hs := spec_pat.parse_one Hs in
   lazymatch Hs with
-  | SSplit ?lr ?Hs =>
+  | SAssert ?lr ?Hs =>
      eapply tac_pvs_assert with _ _ _ _ _ _ lr Hs H Q _;
        [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
         apply _ || fail "iPvsAssert: " P "not a pvs"
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index ad4e4a39fa380803211eac3a00b6c581aac52c8d..6b85e90ad9e56f5bbba3530486651e10f1a59559 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -1,11 +1,12 @@
 From iris.prelude Require Export strings.
 
 Inductive spec_pat :=
-  | SSplit : bool → list string → spec_pat
+  | SAssert : bool → list string → spec_pat
   | SPersistent : spec_pat
   | SPure : spec_pat
   | SAlways : spec_pat
-  | SName : string → spec_pat.
+  | SName : string → spec_pat
+  | SForall : spec_pat.
 
 Module spec_pat.
 Inductive token :=
@@ -15,7 +16,8 @@ Inductive token :=
   | TBracketR : token
   | TPersistent : token
   | TPure : token
-  | TAlways : token.
+  | TAlways : token
+  | TForall : token.
 
 Fixpoint cons_name (kn : string) (k : list token) : list token :=
   match kn with "" => k | _ => TName (string_rev kn) :: k end.
@@ -29,29 +31,31 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
   | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
   | String "!" s => tokenize_go s (TAlways :: cons_name kn k) ""
+  | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
   | String a s => tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
 
-Fixpoint parse_go (ts : list token) (split : option (bool * list string))
+Fixpoint parse_go (ts : list token) (g : option (bool * list string))
     (k : list spec_pat) : option (list spec_pat) :=
-  match split with
+  match g with
   | None =>
      match ts with
      | [] => Some (rev k)
      | TName s :: ts => parse_go ts None (SName s :: k)
      | TMinus :: TBracketL :: ts => parse_go ts (Some (true,[])) k
-     | TMinus :: ts => parse_go ts None (SSplit true [] :: k)
+     | TMinus :: ts => parse_go ts None (SAssert true [] :: k)
      | TBracketL :: ts => parse_go ts (Some (false,[])) k
      | TAlways :: ts => parse_go ts None (SAlways :: k)
      | TPersistent :: ts => parse_go ts None (SPersistent :: k)
      | TPure :: ts => parse_go ts None (SPure :: k)
+     | TForall :: ts => parse_go ts None (SForall :: k)
      | _ => None
      end
   | Some (b, ss) =>
      match ts with
      | TName s :: ts => parse_go ts (Some (b,s :: ss)) k
-     | TBracketR :: ts => parse_go ts None (SSplit b (rev ss) :: k)
+     | TBracketR :: ts => parse_go ts None (SAssert b (rev ss) :: k)
      | _ => None
      end
   end.
diff --git a/proofmode/sts.v b/proofmode/sts.v
index 636f8fee5061aaa56e9ce6b3b39ecade63d3be95..d234c5dec6a6aa4c8bab2d9ec89b812e444f4b36 100644
--- a/proofmode/sts.v
+++ b/proofmode/sts.v
@@ -18,7 +18,8 @@ Lemma tac_sts_fsa {A} (fsa : FSA Λ _ A) fsaV Δ E N i γ S T Q Φ :
       ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★ (sts_own γ s' T' -★ Φ a))) →
   Δ ⊢ Q.
 Proof.
-  intros ????? HΔ'. rewrite -(fsa_split Q); eapply (sts_fsaS φ fsa); eauto.
+  intros ????? HΔ'. rewrite -(fsa_split Q) -(sts_fsaS φ fsa) //.
+  rewrite // -always_and_sep_l. apply and_intro; first done.
   rewrite envs_lookup_sound //; simpl; apply sep_mono_r.
   apply forall_intro=>s; apply wand_intro_l.
   rewrite -assoc; apply const_elim_sep_l=> Hs.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index beb2db7a532e99edb32899b3c0f0190decff7208..8fad7e78684f3c4aff74af7cf5fdf641f0cf2a10 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns.
 From iris.algebra Require Export upred.
 From iris.proofmode Require Export notation.
-From iris.prelude Require Import stringmap.
+From iris.prelude Require Import stringmap hlist.
 
 Declare Reduction env_cbv := cbv [
   env_lookup env_fold env_lookup_delete env_delete env_app
@@ -11,23 +11,25 @@ Declare Reduction env_cbv := cbv [
   bool_eq_dec bool_rec bool_rect bool_dec eqb andb (* bool *)
   assci_eq_dec ascii_to_digits Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
   string_eq_dec string_rec string_rect (* strings *)
+  himpl happly
   env_persistent env_spatial envs_persistent
   envs_lookup envs_lookup_delete envs_delete envs_app
     envs_simple_replace envs_replace envs_split envs_clear_spatial].
 Ltac env_cbv :=
   match goal with |- ?u => let v := eval env_cbv in u in change v end.
 
+(** * Misc *)
 Ltac iFresh :=
   lazymatch goal with
   |- of_envs ?Δ ⊢ _ =>
       match goal with
       | _ => eval vm_compute in (fresh_string_of_set "~" (dom stringset Δ))
+      (* [vm_compute fails] if [Δ] contains evars, so fall-back to [cbv] *)
       | _ => eval cbv in (fresh_string_of_set "~" (dom stringset Δ))
       end
   | _ => constr:"~"
   end.
 
-(** * Misc *)
 Tactic Notation "iTypeOf" constr(H) tactic(tac):=
   let Δ := match goal with |- of_envs ?Δ ⊢ _ => Δ end in
   match eval env_cbv in (envs_lookup H Δ) with
@@ -52,15 +54,13 @@ Tactic Notation "iClear" constr(Hs) :=
   let rec go Hs :=
     match Hs with
     | [] => idtac
+    | "★" :: ?Hs => eapply tac_clear_spatial; [env_cbv; reflexivity|go Hs]
     | ?H :: ?Hs =>
        eapply tac_clear with _ H _ _; (* (i:=H) *)
          [env_cbv; reflexivity || fail "iClear:" H "not found"|go Hs]
     end in
   let Hs := words Hs in go Hs.
 
-Tactic Notation "iClear" "★" :=
-  eapply tac_clear_spatial; [env_cbv; reflexivity|].
-
 (** * Assumptions *)
 Tactic Notation "iExact" constr(H) :=
   eapply tac_assumption with H _ _; (* (i:=H) *)
@@ -97,90 +97,58 @@ Tactic Notation "iAssumption" :=
 
 (** * False *)
 Tactic Notation "iExFalso" := apply tac_ex_falso.
-Tactic Notation "iContradiction" constr(H) := iExFalso; iExact H.
-Tactic Notation "iContradiction" := iExFalso; iAssumption.
-
-(** * Pure introduction *)
-Tactic Notation "iIntro" "{" simple_intropattern(x) "}" :=
-  lazymatch goal with
-  | |- _ ⊢ (∀ _, _) => apply tac_forall_intro; intros x
-  | |- _ ⊢ (?P → _) =>
-     eapply tac_impl_intro_pure;
-       [apply _ || fail "iIntro:" P "not pure"|]; intros x
-  | |- _ ⊢ (?P -★ _) =>
-     eapply tac_wand_intro_pure;
-       [apply _ || fail "iIntro:" P "not pure"|]; intros x
-  | |- _ => intros x
-  end.
-
-(** * Introduction *)
-Tactic Notation "iIntro" constr(H) :=
-  lazymatch goal with
-  | |- _ ⊢ (?Q → _) =>
-    eapply tac_impl_intro with _ H; (* (i:=H) *)
-      [reflexivity || fail "iIntro: introducing " H ":" Q
-                           "into non-empty spatial context"
-      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
-  | |- _ ⊢ (_ -★ _) =>
-    eapply tac_wand_intro with _ H; (* (i:=H) *)
-      [env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
-  | _ => fail "iIntro: nothing to introduce"
-  end.
-
-Tactic Notation "iIntro" "#" constr(H) :=
-  lazymatch goal with
-  | |- _ ⊢ (?P → _) =>
-    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
-      [apply _ || fail "iIntro: " P " not persistent"
-      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
-  | |- _ ⊢ (?P -★ _) =>
-    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
-      [apply _ || fail "iIntro: " P " not persistent"
-      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
-  | _ => fail "iIntro: nothing to introduce"
-  end.
 
 (** * Making hypotheses persistent or pure *)
-Tactic Notation "iPersistent" constr(H) :=
+Local Tactic Notation "iPersistent" constr(H) :=
   eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
     [env_cbv; reflexivity || fail "iPersistent:" H "not found"
     |let Q := match goal with |- ToPersistentP ?Q _ => Q end in
      apply _ || fail "iPersistent:" H ":" Q "not persistent"
     |env_cbv; reflexivity|].
 
-Tactic Notation "iDuplicate" constr(H1) "as" constr(H2) :=
-  eapply tac_duplicate with _ H1 _ H2 _; (* (i:=H1) (j:=H2) *)
-    [env_cbv; reflexivity || fail "iDuplicate:" H1 "not found"
-    |reflexivity || fail "iDuplicate:" H1 "not in persistent context"
-    |env_cbv; reflexivity || fail "iDuplicate:" H2 "not fresh"|].
-Tactic Notation "iDuplicate" "#" constr(H1) "as" constr(H2) :=
-  iPersistent H1; iDuplicate H1 as H2.
-
-Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
+Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
     [env_cbv; reflexivity || fail "iPure:" H "not found"
     |let P := match goal with |- ToPure ?P _ => P end in
      apply _ || fail "iPure:" H ":" P "not pure"
     |intros pat].
-Tactic Notation "iPure" constr(H) := iPure H as ?.
 
-Tactic Notation "iPureIntro" := apply uPred.const_intro.
+Tactic Notation "iPureIntro" :=
+  eapply tac_pure_intro;
+    [let P := match goal with |- ToPure ?P _ => P end in
+     apply _ || fail "iPureIntro:" P "not pure"|].
 
 (** * Specialize *)
-Tactic Notation "iForallSpecialize" constr(H) open_constr(x) :=
-  eapply tac_forall_specialize with _ H _ _ x; (* (i:=H) (a:=x) *)
-    [env_cbv; reflexivity || fail "iSpecialize:" H "not found"
-    |env_cbv; reflexivity|].
+Record iTrm {X As} :=
+  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : string }.
+Arguments ITrm {_ _} _ _ _.
+
+Notation "( H $! x1 .. xn )" :=
+  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 0).
+Notation "( H $! x1 .. xn 'with' pat )" :=
+  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 0).
+Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
+
+Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
+  match xs with
+  | hnil => idtac
+  | _ =>
+    eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *)
+      [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
+      |apply _ || fail 1 "iSpecialize:" H "not a forall of the right arity or type"
+      |env_cbv; reflexivity|]
+  end.
 
-Tactic Notation "iSpecialize" constr (H) constr(pat) :=
+Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
   let solve_to_wand H1 :=
     let P := match goal with |- ToWand ?P _ _ => P end in
     apply _ || fail "iSpecialize:" H1 ":" P "not an implication/wand" in
   let rec go H1 pats :=
     lazymatch pats with
     | [] => idtac
+    | SForall :: ?pats => try (iSpecializeArgs H1 (hcons _ _)); go H1 pats
     | SAlways :: ?pats => iPersistent H1; go H1 pats
-    | SSplit true [] :: SAlways :: ?pats =>
+    | SAssert true [] :: SAlways :: ?pats =>
        eapply tac_specialize_domain_persistent with _ _ H1 _ _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
@@ -201,7 +169,9 @@ Tactic Notation "iSpecialize" constr (H) constr(pat) :=
        eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
          [env_cbv; reflexivity || fail "iSpecialize:" H2 "not found"
          |env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
-         |solve_to_wand H1
+         |let P := match goal with |- ToWand ?P ?Q _ => P end in
+          let Q := match goal with |- ToWand ?P ?Q _ => Q end in
+          apply _ || fail "iSpecialize: cannot instantiate" H1 ":" P "with" H2 ":" Q
          |env_cbv; reflexivity|go H1 pats]
     | SPersistent :: ?pats =>
        eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _;
@@ -211,186 +181,90 @@ Tactic Notation "iSpecialize" constr (H) constr(pat) :=
           apply _ || fail "iSpecialize:" Q "not persistent"
          |env_cbv; reflexivity| |go H1 pats]
     | SPure :: ?pats =>
-       eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _; (* make custom tac_ lemma *)
+       eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _;
+         (* make custom tac_ lemma *)
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |let Q := match goal with |- PersistentP ?Q => Q end in
           apply _ || fail "iSpecialize:" Q "not persistent"
          |env_cbv; reflexivity|iPureIntro|go H1 pats]
-    | SSplit ?lr ?Hs :: ?pats =>
+    | SAssert ?lr ?Hs :: ?pats =>
        eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"|
          |go H1 pats]
-    end in
-  repeat (iForallSpecialize H _);
-  let pats := spec_pat.parse pat in go H pats.
-
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) "}" :=
-  iForallSpecialize H x1.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1)
-    open_constr(x2) "}" :=
-  iSpecialize H { x1 }; iForallSpecialize H x2.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) "}" :=
-  iSpecialize H { x1 x2 }; iForallSpecialize H x3.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) "}" :=
-  iSpecialize H { x1 x2 x3 }; iForallSpecialize H x4.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-     open_constr(x3) open_constr(x4) open_constr(x5) "}" :=
-  iSpecialize H { x1 x2 x3 x4 }; iForallSpecialize H x5.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 }; iForallSpecialize H x6.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 }; iForallSpecialize H x7.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) open_constr(x8) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; iForallSpecialize H x8.
-
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) "}" constr(Hs) :=
-  iSpecialize H { x1 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2) "}"
-    constr(Hs) :=
-  iSpecialize H { x1 x2 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}"
-    constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; iSpecialize H @ Hs.
-Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) open_constr(x8) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 x8 }; iSpecialize H @ Hs.
+    end in let pats := spec_pat.parse pat in go H pats.
+
+Tactic Notation "iSpecialize" open_constr(t) :=
+  match t with
+  | ITrm ?H ?xs ?pat => iSpecializeArgs H xs; iSpecializePat H pat
+  end.
 
 (** * Pose proof *)
-Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
-  eapply tac_pose_proof with _ H _; (* (j:=H) *)
-    [first
-       [eapply lem
-       |apply uPred.entails_impl; eapply lem
-       |apply uPred.equiv_iff; eapply lem]
-    |env_cbv; reflexivity || fail "iPoseProof:" H "not fresh"|].
-
-Tactic Notation "iPoseProof" open_constr(lem) constr(Hs) "as" constr(H) :=
-  iPoseProof lem as H; last iSpecialize H Hs.
-
-Tactic Notation "iPoseProof" open_constr(lem) :=
-  let H := iFresh in iPoseProof lem as H.
-Tactic Notation "iPoseProof" open_constr(lem) constr(Hs) :=
-  let H := iFresh in iPoseProof lem Hs as H.
-
-Tactic Notation "iPoseProof" open_constr(lem) "as" tactic(tac) :=
-  lazymatch type of lem with
-  | string => tac lem
-  | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
+  lazymatch type of H1 with
+  | string =>
+     eapply tac_pose_proof_hyp with _ _ H1 _ H2 _;
+       [env_cbv; reflexivity || fail "iPoseProof:" H1 "not found"
+       |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
+  | _ =>
+     eapply tac_pose_proof with _ H2 _ _ _; (* (j:=H) *)
+       [first [eapply H1|apply uPred.equiv_iff; eapply H1]
+       |apply _
+       |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
+  end.
+
+Tactic Notation "iPoseProof" open_constr(t) "as" constr(H) :=
+  lazymatch t with
+  | ITrm ?H1 ?xs ?pat =>
+     iPoseProofCore H1 as H; last (iSpecializeArgs H xs; iSpecializePat H pat)
+  | _ => iPoseProofCore t as H
   end.
 
-Tactic Notation "iPoseProof" open_constr(lem) constr(Hs) "as" tactic(tac) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs; last tac H).
+Tactic Notation "iPoseProof" open_constr(t) :=
+  let H := iFresh in iPoseProof t as H.
 
 (** * Apply *)
-Tactic Notation "iApply" open_constr (lem) :=
-  iPoseProof lem as (fun H => repeat (iForallSpecialize H _); first
-    [iExact H
-    |eapply tac_apply with _ H _ _ _;
-       [env_cbv; reflexivity || fail 1 "iApply:" lem "not found"
-       |apply _ || fail 1 "iApply: cannot apply" lem|]]).
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) "}" :=
-  iSpecialize H { x1 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1)
-    open_constr(x2) "}" :=
-  iSpecialize H { x1 x2 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) "}" :=
-  iSpecialize H { x1 x2 x3 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) "}" :=
-  iSpecialize H { x1 x2 x3 x4 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-     open_constr(x3) open_constr(x4) open_constr(x5) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; last iApply H.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) open_constr(x8) "}" :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 x8 }; last iApply H.
-
-(* this is wrong *)
-Tactic Notation "iApply" open_constr (lem) constr(Hs) :=
-  iPoseProof lem Hs as (fun H => first
-    [iExact H
-    |eapply tac_apply with _ H _ _ _;
-       [env_cbv; reflexivity || fail 1 "iApply:" lem "not found"
-       |apply _ || fail 1 "iApply: cannot apply" lem|]]).
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) "}" constr(Hs) :=
-  iSpecialize H { x1 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2) "}"
-    constr(Hs) :=
-  iSpecialize H { x1 x2 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}"
-    constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; last iApply H Hs.
-Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
-    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
-    open_constr(x7) open_constr(x8) "}" constr(Hs) :=
-  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 x8 }; last iApply H Hs.
+Tactic Notation "iApplyCore" constr(H) := first
+  [iExact H
+  |eapply tac_apply with _ H _ _ _;
+     [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
+     |apply _ || fail 1 "iApply: cannot apply" H|]].
+
+Tactic Notation "iApply" open_constr(t) :=
+  let Htmp := iFresh in
+  lazymatch t with
+  | ITrm ?H ?xs ?pat =>
+     iPoseProofCore H as Htmp; last (
+       iSpecializeArgs Htmp xs;
+       try (iSpecializeArgs Htmp (hcons _ _));
+       iSpecializePat Htmp pat; last iApplyCore Htmp)
+  | _ =>
+     iPoseProofCore t as Htmp; last (
+       try (iSpecializeArgs Htmp (hcons _ _));
+       iApplyCore Htmp)
+  end; try apply _.
 
 (** * Revert *)
-Tactic Notation "iRevert" "★" := eapply tac_revert_spatial; env_cbv.
-
-Tactic Notation "iForallRevert" ident(x) :=
+Local Tactic Notation "iForallRevert" ident(x) :=
   let A := type of x in
   lazymatch type of A with
   | Prop => revert x; apply tac_pure_revert
   | _ => revert x; apply tac_forall_revert
   end || fail "iRevert: cannot revert" x.
 
-Tactic Notation "iImplRevert" constr(H) :=
-  eapply tac_revert with _ H _ _; (* (i:=H) *)
-    [env_cbv; reflexivity || fail "iRevert:" H "not found"
-    |env_cbv].
-
 Tactic Notation "iRevert" constr(Hs) :=
   let rec go H2s :=
-    match H2s with [] => idtac | ?H2 :: ?H2s => go H2s; iImplRevert H2 end in
+    match H2s with
+    | [] => idtac
+    | "★" :: ?H2s => go H2s; eapply tac_revert_spatial; env_cbv
+    | ?H2 :: ?H2s =>
+       go H2s;
+       eapply tac_revert with _ H2 _ _; (* (i:=H2) *)
+         [env_cbv; reflexivity || fail "iRevert:" H2 "not found"
+         |env_cbv]
+    end in
   let Hs := words Hs in go Hs.
 
 Tactic Notation "iRevert" "{" ident(x1) "}" :=
@@ -446,7 +320,7 @@ Tactic Notation "iRight" :=
     [let P := match goal with |- OrSplit ?P _ _ => P end in
      apply _ || fail "iRight:" P "not a disjunction"|].
 
-Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
+Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
   eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [env_cbv; reflexivity || fail "iOrDestruct:" H "not found"
     |let P := match goal with |- OrDestruct ?P _ _ => P end in
@@ -476,7 +350,7 @@ Tactic Notation "iSplitR" constr(Hs) :=
 Tactic Notation "iSplitL" := iSplitR "".
 Tactic Notation "iSplitR" := iSplitL "".
 
-Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
+Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
   eapply tac_sep_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [env_cbv; reflexivity || fail "iSepDestruct:" H "not found"
     |let P := match goal with |- SepDestruct _ ?P _ _ => P end in
@@ -533,25 +407,28 @@ Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
     uconstr(x8) :=
   iExists x1; iExists x2, x3, x4, x5, x6, x7, x8.
 
-Tactic Notation "iExistDestruct" constr(H) "as" ident(x) constr(Hx) :=
+Local Tactic Notation "iExistDestruct" constr(H)
+    "as" simple_intropattern(x) constr(Hx) :=
   eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
     [env_cbv; reflexivity || fail "iExistDestruct:" H "not found"
     |let P := match goal with |- ExistDestruct ?P _ => P end in
      apply _ || fail "iExistDestruct:" H ":" P "not an existential"|];
-  intros x; eexists; split;
-    [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"|].
+  let y := fresh in
+  intros y; eexists; split;
+    [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"
+    |revert y; intros x].
 
 (** * Destruct tactic *)
-Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
+Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
   let rec go Hz pat :=
     lazymatch pat with
     | IAnom => idtac
-    | IAnomPure => iPure Hz
-    | IClear => iClear Hz
+    | IAnomPure => iPure Hz as ?
+    | IDrop => iClear Hz
     | IFrame => iFrame Hz
     | IName ?y => iRename Hz into y
     | IPersistent ?pat => iPersistent Hz; go Hz pat
-    | IList [[]] => iContradiction Hz
+    | IList [[]] => iExFalso; iExact Hz
     | IList [[?pat1; ?pat2]] =>
        let Hy := iFresh in iSepDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
     | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
@@ -559,126 +436,91 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
     end
   in let pat := intro_pat.parse_one pat in go H pat.
 
-Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1) "}"
+Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1) "}"
     constr(pat) :=
   iExistDestruct H as x1 H; iDestructHyp H as @ pat.
-Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) "}" constr(pat) :=
   iExistDestruct H as x1 H; iDestructHyp H as { x2 } pat.
-Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
   iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 } pat.
-Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
     constr(pat) :=
   iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 } pat.
-Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) "}" constr(pat) :=
   iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 } pat.
-Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
   iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 } pat.
-Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
     constr(pat) :=
   iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 x7 } pat.
-Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
     simple_intropattern(x8) "}" constr(pat) :=
   iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 x7 x8 } pat.
 
+Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) :=
+  lazymatch type of lem with
+  | string => tac lem
+  | iTrm =>
+     lazymatch lem with
+     | @iTrm string ?H _ hnil ?pat =>
+        iSpecializePat H pat; last tac H
+     | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+     end
+  | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+  end.
+
 Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as pat).
+  iDestructHelp H as (fun H => iDestructHyp H as pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) "}"
     constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) "}" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
     constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) "}" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
     constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
 Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
     simple_intropattern(x8) "}" constr(pat) :=
-  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
-
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs; last iDestructHyp H as pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) "}"
-    constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 x4 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) "}"
-    constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
-    simple_intropattern(x7) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
-Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
-    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
-    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
-    simple_intropattern(x7) simple_intropattern(x8) "}" constr(pat) :=
-  iPoseProof lem as (fun H => iSpecialize H Hs;
-    last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
+  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
 
 Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
-  let Htmp := iFresh in iDestruct H as Htmp; iPure Htmp as pat.
-Tactic Notation "iDestruct" open_constr(H) constr(Hs)
-    "as" "%" simple_intropattern(pat) :=
-  let Htmp := iFresh in iDestruct H Hs as Htmp; iPure Htmp as pat.
+  let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat.
 
 (** * Always *)
 Tactic Notation "iAlways":=
-   apply tac_always_intro;
-     [reflexivity || fail "iAlways: spatial context non-empty"|].
+  apply tac_always_intro;
+    [reflexivity || fail "iAlways: spatial context non-empty"|].
 
 (** * Later *)
 Tactic Notation "iNext":=
@@ -688,13 +530,65 @@ Tactic Notation "iNext":=
      apply _ || fail "iNext:" P "does not contain laters"|].
 
 (** * Introduction tactic *)
+Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := first
+  [ (* (∀ _, _) *) apply tac_forall_intro; intros x
+  | (* (?P → _) *) eapply tac_impl_intro_pure;
+     [let P := match goal with |- ToPure ?P _ => P end in
+      apply _ || fail "iIntro:" P "not pure"
+     |intros x]
+  | (* (?P -★ _) *) eapply tac_wand_intro_pure;
+     [let P := match goal with |- ToPure ?P _ => P end in
+      apply _ || fail "iIntro:" P "not pure"
+     |intros x]
+  |intros x].
+
+Local Tactic Notation "iIntro" constr(H) := first
+  [ (* (?Q → _) *)
+    eapply tac_impl_intro with _ H; (* (i:=H) *)
+      [reflexivity || fail 1 "iIntro: introducing" H
+                             "into non-empty spatial context"
+      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
+  | (* (_ -★ _) *)
+    eapply tac_wand_intro with _ H; (* (i:=H) *)
+      [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
+  | fail 1 "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntro" "#" constr(H) := first
+  [ (* (?P → _) *)
+    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
+      [let P := match goal with |- ToPersistentP ?P _ => P end in
+       apply _ || fail 1 "iIntro: " P " not persistent"
+      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
+  | (* (?P -★ _) *)
+    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
+      [let P := match goal with |- ToPersistentP ?P _ => P end in
+       apply _ || fail 1 "iIntro: " P " not persistent"
+      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
+  | fail 1 "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntroForall" :=
+  lazymatch goal with
+  | |- ∀ _, ?P => fail
+  | |- ∀ _, _ => intro
+  | |- _ ⊢ (∀ x : _, _) => iIntro {x}
+  end.
+Local Tactic Notation "iIntro" :=
+  lazymatch goal with
+  | |- _ → ?P => intro
+  | |- _ ⊢ (_ -★ _) => iIntro {?} || let H := iFresh in iIntro #H || iIntro H
+  | |- _ ⊢ (_ → _) => iIntro {?} || let H := iFresh in iIntro #H || iIntro H
+  end.
+
 Tactic Notation "iIntros" constr(pat) :=
   let rec go pats :=
     lazymatch pats with
     | [] => idtac
+    | IForall :: ?pats => repeat iIntroForall; go pats
+    | IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
     | ISimpl :: ?pats => simpl; go pats
     | IAlways :: ?pats => iAlways; go pats
     | INext :: ?pats => iNext; go pats
+    | IClear ?Hs :: ?pats => iClear Hs; go pats
     | IPersistent (IName ?H) :: ?pats => iIntro #H; go pats
     | IName ?H :: ?pats => iIntro H; go pats
     | IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
@@ -707,6 +601,7 @@ Tactic Notation "iIntros" constr(pat) :=
     | _ => fail "iIntro: failed with" pats
     end
   in let pats := intro_pat.parse pat in try iProof; go pats.
+Tactic Notation "iIntros" := iIntros "**".
 
 Tactic Notation "iIntros" "{" simple_intropattern(x1) "}" :=
   try iProof; iIntro { x1 }.
@@ -766,55 +661,55 @@ Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
 
 (* This is pretty ugly, but without Ltac support for manipulating lists of
 idents I do not know how to do this better. *)
-Ltac iLöbCore IH tac_before tac_after :=
+Local Ltac iLöbHelp IH tac_before tac_after :=
   match goal with
   | |- of_envs ?Δ ⊢ _ =>
-     let Hs := constr:(rev (env_dom_list (env_spatial Δ))) in
-     iRevert ★; tac_before;
+     let Hs := constr:(reverse (env_dom_list (env_spatial Δ))) in
+     iRevert ["★"]; tac_before;
      eapply tac_löb with _ IH;
        [reflexivity
        |env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|];
-    tac_after;  iIntros Hs
+    tac_after; iIntros Hs
   end.
 
-Tactic Notation "iLöb" "as" constr (IH) := iLöbCore IH idtac idtac.
+Tactic Notation "iLöb" "as" constr (IH) := iLöbHelp IH idtac idtac.
 Tactic Notation "iLöb" "{" ident(x1) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 }) ltac:(iIntros { x1 }).
+  iLöbHelp IH ltac:(iRevert { x1 }) ltac:(iIntros { x1 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 }) ltac:(iIntros { x1 x2 }).
+  iLöbHelp IH ltac:(iRevert { x1 x2 }) ltac:(iIntros { x1 x2 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 }) ltac:(iIntros { x1 x2 x3 }).
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 }) ltac:(iIntros { x1 x2 x3 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}" "as"
     constr (IH):=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 }) ltac:(iIntros { x1 x2 x3 x4 }).
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 }) ltac:(iIntros { x1 x2 x3 x4 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 })
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 })
               ltac:(iIntros { x1 x2 x3 x4 x5 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) ident(x6) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 })
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 })
               ltac:(iIntros { x1 x2 x3 x4 x5 x6 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) ident(x6) ident(x7) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 })
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 })
               ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
     ident(x5) ident(x6) ident(x7) ident(x8) "}" "as" constr (IH) :=
-  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 x8 })
+  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 x8 })
               ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }).
 
 (** * Assert *)
 Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
   let H := iFresh in
-  let Hs := spec_pat.parse_one Hs in
+  let Hs := spec_pat.parse Hs in
   lazymatch Hs with
-  | SSplit ?lr ?Hs =>
+  | [SAssert ?lr ?Hs] =>
      eapply tac_assert with _ _ _ lr Hs H Q; (* (js:=Hs) (j:=H) (P:=Q) *)
        [env_cbv; reflexivity || fail "iAssert:" Hs "not found"
        |env_cbv; reflexivity|
        |iDestructHyp H as pat]
-  | SPersistent =>
+  | [SAssert true [] :: SAlways]  =>
      eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
        [apply _ || fail "iAssert:" Q "not persistent"
        |env_cbv; reflexivity|
@@ -825,24 +720,27 @@ Tactic Notation "iAssert" constr(Q) "as" constr(pat) :=
   iAssert Q as pat with "[]".
 
 (** * Rewrite *)
-Ltac iRewriteFindPred :=
+Local Ltac iRewriteFindPred :=
   match goal with
   | |- _ ⊣⊢ ?Φ ?x =>
      generalize x;
      match goal with |- (∀ y, @?Ψ y ⊣⊢ _) => unify Φ Ψ; reflexivity end
   end.
 
-Tactic Notation "iRewriteCore" constr(lr) constr(Heq) :=
+Local Tactic Notation "iRewriteCore" constr(lr) open_constr(t) :=
+  let Heq := iFresh in iPoseProof t as Heq; last (
   eapply (tac_rewrite _ Heq _ _ lr);
     [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
     |let P := match goal with |- ?P ⊢ _ => P end in
      reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
     |iRewriteFindPred
-    |intros ??? ->; reflexivity|lazy beta].
-Tactic Notation "iRewrite" constr(Heq) := iRewriteCore false Heq.
-Tactic Notation "iRewrite" "-" constr(Heq) := iRewriteCore true Heq.
+    |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
+
+Tactic Notation "iRewrite" open_constr(t) := iRewriteCore false t.
+Tactic Notation "iRewrite" "-" open_constr(t) := iRewriteCore true t.
 
-Tactic Notation "iRewriteCore" constr(lr) constr(Heq) "in" constr(H) :=
+Local Tactic Notation "iRewriteCore" constr(lr) open_constr(t) "in" constr(H) :=
+  let Heq := iFresh in iPoseProof t as Heq; last (
   eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
     [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
     |env_cbv; reflexivity || fail "iRewrite:" H "not found"
@@ -850,12 +748,13 @@ Tactic Notation "iRewriteCore" constr(lr) constr(Heq) "in" constr(H) :=
      reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
     |iRewriteFindPred
     |intros ??? ->; reflexivity
-    |env_cbv; reflexivity|lazy beta].
-Tactic Notation "iRewrite" constr(Heq) "in" constr(H) :=
-  iRewriteCore false Heq in H.
-Tactic Notation "iRewrite" "-" constr(Heq) "in" constr(H) :=
-  iRewriteCore true Heq in H.
+    |env_cbv; reflexivity|lazy beta; iClear Heq]).
+
+Tactic Notation "iRewrite" open_constr(t) "in" constr(H) :=
+  iRewriteCore false t in H.
+Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
+  iRewriteCore true t in H.
 
 (* Make sure that by and done solve trivial things in proof mode *)
-Hint Extern 0 (of_envs _ ⊢ _) => by apply tac_pure_intro.
+Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
 Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
index 36ecbd2cd312238219348d818544fa5ad0538abf..ab3d1f0ea35a2796a5928e3b9750bb89145e070f 100644
--- a/proofmode/weakestpre.v
+++ b/proofmode/weakestpre.v
@@ -8,7 +8,7 @@ Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 
-Instance frame_wp E e R Φ mΨ :
+Global Instance frame_wp E e R Φ mΨ :
   (∀ v, Frame R (Φ v) (mΨ v)) →
   Frame R (WP e @ E {{ Φ }})
           (Some (WP e @ E {{ v, if mΨ v is Some Q then Q else True }}))%I.
@@ -17,6 +17,3 @@ Global Instance fsa_split_wp E e Φ :
   FSASplit (WP e @ E {{ Φ }})%I E (wp_fsa e) (language.atomic e) Φ.
 Proof. split. done. apply _. Qed.
 End weakestpre.
-
-Hint Extern 10 (Frame _ (WP _ @ _ {{ _ }}) _) =>
-  class_apply frame_wp : typeclass_instances.
\ No newline at end of file
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 45366e9e0aef6f5b0f923d78088d3f3229524be3..ca07236f2934682a3f01dc886718d89070dad283 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -11,6 +11,7 @@ Definition client : expr [] :=
   let: "b" := ^newbarrier #() in
   ('"y" <- (λ: "z", '"z" + #42) ;; ^signal '"b") ||
     (^(worker 12) '"b" '"y" || ^(worker 17) '"b" '"y").
+Global Opaque worker client.
 
 Section client.
   Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
@@ -48,9 +49,9 @@ Section client.
       iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
       iSplitL; [|by iIntros {_ _} "_ >"].
-      iDestruct recv_weaken "[] Hr" as "Hr".
-      { iIntros "Hy". by iApply y_inv_split "Hy". }
-      iPvs recv_split "Hr" as "[H1 H2]"; first done.
+      iDestruct (recv_weaken with "[] Hr") as "Hr".
+      { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
+      iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
       iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); eauto.
       iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|by iIntros {_ _} "_ >"]];
         iApply worker_safe; by iSplit.
@@ -64,7 +65,7 @@ Section ClosedProofs.
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ v, True }}.
   Proof.
     iIntros "! Hσ".
-    iPvs (heap_alloc (nroot .@ "Barrier")) "Hσ" as {h} "[#Hh _]"; first done.
+    iPvs (heap_alloc (nroot .@ "Barrier") with "Hσ") as {h} "[#Hh _]"; first done.
     iApply (client_safe (nroot .@ "Barrier") (nroot .@ "Heap")); auto with ndisj.
   Qed.
 
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 10a4979167fc98f5c98c5584f0322610cd83a053..f83c8a8d739a4ec2b2222f1053a774fe4b6cdcbc 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -27,7 +27,7 @@ Section LiftingTests.
      nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ v, v = #2 }}.
   Proof.
     iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
-    wp_alloc l as "Hl". wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
+    wp_alloc l. wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
   Qed.
 
   Definition FindPred : val :=
@@ -37,6 +37,7 @@ Section LiftingTests.
   Definition Pred : val :=
     λ: "x",
       if: '"x" ≤ #0 then -^FindPred (-'"x" + #2) #0 else ^FindPred '"x" #0.
+  Global Opaque FindPred Pred.
 
   Lemma FindPred_spec n1 n2 E Φ :
     n1 < n2 →
@@ -44,8 +45,8 @@ Section LiftingTests.
   Proof.
     iIntros {Hn} "HΦ". iLöb {n1 Hn} as "IH".
     wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
-    - iApply "IH" "% HΦ". omega.
-    - iPvsIntro. by assert (n1 = n2 - 1) as -> by omega.
+    - iApply ("IH" with "% HΦ"). omega.
+    - iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega.
   Qed.
 
   Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊢ WP Pred #n @ E {{ Φ }}.
@@ -69,7 +70,7 @@ Section ClosedProofs.
   Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ v, v = #2 }}.
   Proof.
     iProof. iIntros "! Hσ".
-    iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot.
+    iPvs (heap_alloc nroot with "Hσ") as {h} "[? _]"; first by rewrite nclose_nroot.
     iApply heap_e_spec; last done; by rewrite nclose_nroot.
   Qed.
 End ClosedProofs.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index a96ddeaf7af674235b5f3209f8a621812deb08f1..969586fdfc58924cc7da9010ed137109ca7654bf 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -7,6 +7,7 @@ Import uPred.
 Definition client eM eW1 eW2 : expr [] :=
   let: "b" := newbarrier #() in
   (eM ;; ^signal '"b") || ((^wait '"b" ;; eW1) || (^wait '"b" ;; eW2)).
+Global Opaque client.
 
 Section proof.
 Context (G : cFunctor).
@@ -24,7 +25,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp) :
 Proof.
   iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
   iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
-  wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He" "!"].
+  wp_seq. iApply wp_wand_l. iSplitR; [|by iApply ("He" with "!")].
   iIntros {v} "?"; iExists x; by iSplit.
 Qed.
 
@@ -35,14 +36,14 @@ Context {Ψ_join  : ∀ x, (Ψ1 x ★ Ψ2 x) ⊢ Ψ x}.
 Lemma P_res_split γ : barrier_res γ Φ ⊢ (barrier_res γ Φ1 ★ barrier_res γ Φ2).
 Proof.
   iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
-  iDestruct Φ_split "Hx" as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
+  iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
 Qed.
 
 Lemma Q_res_join γ : (barrier_res γ Ψ1 ★ barrier_res γ Ψ2) ⊢ ▷ barrier_res γ Ψ.
 Proof.
   iIntros "[Hγ Hγ']";
   iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']".
-  iDestruct (one_shot_agree γ x x') "- !" as "Hxx"; first (by iSplit).
+  iDestruct (one_shot_agree γ x x' with "- !") as "Hxx"; first (by iSplit).
   iNext. iRewrite -"Hxx" in "Hx'".
   iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx".
 Qed.
@@ -62,20 +63,20 @@ Proof.
   set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I).
   wp_let. wp_apply (wp_par _ _ (λ _, True)%I workers_post); first done.
   iFrame "Hh". iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
-  - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|iApply "He" "HP"].
+  - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
     iIntros {v} "HP"; iDestruct "HP" as {x} "HP". wp_let.
-    iPvs (one_shot_init _ _ x) "Hγ" as "Hx".
+    iPvs (one_shot_init _ _ x with "Hγ") as "Hx".
     iApply signal_spec; iFrame "Hs"; iSplit; last done.
     iExists x; by iSplitL "Hx".
-  - iDestruct recv_weaken "[] Hr" as "Hr".
-    { iIntros "?". by iApply P_res_split "-". }
-    iPvs recv_split "Hr" as "[H1 H2]"; first done.
+  - iDestruct (recv_weaken with "[] Hr") as "Hr".
+    { iIntros "?". by iApply (P_res_split with "-"). }
+    iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
     wp_apply (wp_par _ _ (λ _, barrier_res γ Ψ1)%I
       (λ _, barrier_res γ Ψ2)%I); first done.
     iSplit; [done|]; iSplitL "H1"; [|iSplitL "H2"].
     + by iApply worker_spec; iSplitL "H1".
     + by iApply worker_spec; iSplitL "H2".
     + by iIntros {v1 v2} "? >".
-  - iIntros {_ v} "[_ H]"; iPoseProof Q_res_join "H". by iNext; iExists γ.
+  - iIntros {_ v} "[_ H]"; iPoseProof (Q_res_join with "H"). by iNext; iExists γ.
 Qed.
 End proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 7fa38345bf1a987caca629049822b87461a88d23..89dd05d948ffbf573e55ebb8b388f27f5451fc9c 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -18,6 +18,7 @@ Definition one_shot_example : val := λ: <>,
        | InjR "m" => Assert ('"n" = '"m")
        end
     end)).
+Global Opaque one_shot_example.
 
 Class one_shotG Σ :=
   OneShotG { one_shot_inG :> inG heap_lang Σ (one_shotR (dec_agreeR Z)) }.
@@ -44,13 +45,13 @@ Proof.
   iIntros "[#? Hf] /=".
   rewrite /one_shot_example. wp_seq. wp_alloc l as "Hl". wp_let.
   iPvs (own_alloc OneShotPending) as {γ} "Hγ"; first done.
-  iPvs (inv_alloc N _ (one_shot_inv γ l)) "[Hl Hγ]" as "#HN"; first done.
+  iPvs (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN"; first done.
   { iNext. iLeft. by iSplitL "Hl". }
   iPvsIntro. iApply "Hf"; iSplit.
   - iIntros {n} "!". wp_let.
     iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
     + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft; iPvsIntro].
-      iPvs own_update "Hγ" as "Hγ".
+      iPvs (own_update with "Hγ") as "Hγ".
       { (* FIXME: canonical structures are not working *)
         by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)). }
       iPvsIntro; iRight; iExists n; by iSplitL "Hl".
@@ -72,10 +73,10 @@ Proof.
     { wp_case. wp_seq. by iPvsIntro. }
     wp_case. wp_let. wp_focus (! _)%E.
     iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
-    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%". }
+    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
     wp_load.
     iCombine "Hγ" "Hγ'" as "Hγ".
-    iDestruct own_valid "Hγ !" as % [=->]%dec_agree_op_inv.
+    iDestruct (own_valid with "Hγ !") as % [=->]%dec_agree_op_inv.
     iSplitL "Hl"; [iRight; iExists m; by iSplit|].
     wp_case. wp_let. iApply wp_assert'. wp_op=>?; simplify_eq/=.
     iSplit. done. by iNext.
@@ -90,7 +91,7 @@ Lemma hoare_one_shot (Φ : val → iProp) :
 Proof.
   iIntros "#? ! _". iApply wp_one_shot. iSplit; first done.
   iIntros {f1 f2} "[#Hf1 #Hf2]"; iSplit.
-  - iIntros {n} "! _". wp_proj. iApply "Hf1" "!".
+  - iIntros {n} "! _". wp_proj. iApply ("Hf1" with "!").
   - iIntros "! _". wp_proj.
     iApply wp_wand_l; iFrame "Hf2". by iIntros {v} "#? ! _".
 Qed.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 288c75c678a7cb696c4835bbf9dca4ac9842d957..8146ab1158e1e817638df0621ba6604ad016a421 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,26 +1,37 @@
 From iris.proofmode Require Import tactics.
 
+Lemma demo_0 {M : cmraT} (P Q : uPred M) :
+  □ (P ∨ Q) ⊢ ((∀ x, x = 0 ∨ x = 1) → (Q ∨ P)).
+Proof.
+  iIntros "#H #H2".
+  (* should remove the disjunction "H" *)
+  iDestruct "H" as "[?|?]"; last by iLeft.
+  (* should keep the disjunction "H" because it is instantiated *)
+  iDestruct ("H2" $! 10) as "[%|%]". done. done.
+Qed.
+
 Lemma demo_1 (M : cmraT) (P1 P2 P3 : nat → uPred M) :
   True ⊢ (∀ (x y : nat) a b,
     x ≡ y →
     □ (uPred_ownM (a ⋅ b) -★
     (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -★
-    ▷ (∀ z, P2 z) -★
+    □ ▷ (∀ z, P2 z ∨ True → P2 z) -★
     ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (n = n ↔ P3 n))) -★
     ▷ (x = 0) ∨ ∃ x z, ▷ P3 (x + z) ★ uPred_ownM b ★ uPred_ownM (core b))).
 Proof.
-  iIntros {i [|j] a b ?} "! [Ha Hb] H1 H2 H3"; setoid_subst.
+  iIntros {i [|j] a b ?} "! [Ha Hb] H1 #H2 H3"; setoid_subst.
   { iLeft. by iNext. }
   iRight.
   iDestruct "H1" as {z1 z2 c} "(H1&_&#Hc)".
-  iRevert {a b} "Ha Hb". iIntros {b a} "Hb Ha".
+  iPoseProof "Hc" as "foo".
+  iRevert {a b} "Ha Hb". iIntros {b a} "Hb {foo} Ha".
   iAssert (uPred_ownM (a â‹… core a))%I as "[Ha #Hac]" with "[Ha]".
   { by rewrite cmra_core_r. }
   iFrame "Ha Hac".
   iExists (S j + z1), z2.
   iNext.
-  iApply "H3" { _ 0 } "H1 ! [H2] !".
-  - iSplit. done. iApply "H2".
+  iApply ("H3" $! _ 0 with "H1 ! [] !").
+  - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
   - done.
 Qed.
 
@@ -43,4 +54,28 @@ Qed.
 
 Lemma demo_3 (M : cmraT) (P1 P2 P3 : uPred M) :
   (P1 ★ P2 ★ P3) ⊢ (▷ P1 ★ ▷ (P2 ★ ∃ x, (P3 ∧ x = 0) ∨ P3)).
-Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.
\ No newline at end of file
+Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.
+
+Definition foo {M} (P : uPred M) := (P → P)%I.
+Definition bar {M} : uPred M := (∀ P, foo P)%I.
+
+Lemma demo_4 (M : cmraT) : True ⊢ @bar M.
+Proof. iIntros. iIntros {P} "HP". done. Qed.
+
+Lemma demo_5 (M : cmraT) (x y : M) (P : uPred M) :
+  (∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)).
+Proof.
+  iIntros "H1 H2".
+  iRewrite (uPred.eq_sym x x with "- !"). iApply uPred.eq_refl.
+  iRewrite -("H1" $! _ with "- !"); first done.
+  iApply uPred.eq_refl.
+Qed.
+
+Lemma demo_6 (M : cmraT) (P Q : uPred M) :
+  True ⊢ (∀ x y z : nat,
+    x = plus 0 x → y = 0 → z = 0 → P → □ Q → foo (x ≡ x)).
+Proof.
+  iIntros {a} "*".
+  iIntros "#Hfoo **".
+  by iIntros "# _".
+Qed.