diff --git a/CHANGELOG.md b/CHANGELOG.md
index 10ed7959b0bee06177b33ff05e287f3ddae229b5..a3305d69634e1c382924d143fb521dd6bccb7616 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,6 +18,7 @@ Changes in Coq:
 
 * Rename some things and change notation:
   - The unit of a camera: `empty` -> `unit`, `∅` -> `ε`
+  - Disjointness: `⊥` -> `##`
   - A proof mode type class `IntoOp` -> `IsOp`
   - OFEs with all elements being discrete: `Discrete` -> `OfeDiscrete`
   - OFE elements whose equality is discrete: `Timeless` -> `Discrete`
@@ -85,6 +86,8 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
   of evars, which often led to divergence. There are a few places where type
   annotations are now needed.
 * Move the `prelude` folder to its own project: std++
+* The rules `internal_eq_rewrite` and `internal_eq_rewrite_contractive` are now
+  stated in the logic, i.e. they are `iApply` friendly.
 
 ## Iris 3.0.0 (released 2017-01-11)
 
@@ -113,7 +116,7 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
 * Slightly weaker notion of atomicity: an expression is atomic if it reduces in
   one step to something that does not reduce further.
 * Changed notation for embedding Coq assertions into Iris.  The new notation is
-  ⌜φ⌝.  Also removed `=` and `##` from the Iris scope.  (The old notations are
+  ⌜φ⌝.  Also removed `=` and `⊥` from the Iris scope.  (The old notations are
   provided in `base_logic.deprecated`.)
 * Up-closure of namespaces is now a notation (↑) instead of a coercion.
 * With invariants and the physical state being handled in the logic, there is no
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index 66ccfc940da956981455546ec6d92a7a2c0b5121..b6925ba58c8518c2f6a73ad74833861073ff9578 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -55,7 +55,7 @@ done
 # Upgrade cached things.
 echo
 echo "[opam-ci] Upgrading opam"
-opam upgrade -y --fixup
+opam upgrade -y --fixup && opam upgrade -y
 
 # Install build-dependencies.
 echo
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 394212c45de024cffcab1ebc49432ddcf8b4217f..96b4ce2d97186e32aada729673f93e75c0a5dcae 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -9,7 +9,7 @@ Module Import uPred.
 End uPred.
 
 (* Hint DB for the logic *)
-Hint Resolve pure_intro.
+Hint Resolve pure_intro : I.
 Hint Resolve or_elim or_intro_l' or_intro_r' : I.
 Hint Resolve and_intro and_elim_l' and_elim_r' : I.
 Hint Resolve persistently_mono : I.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 5449c5bec6913364b3c54119b9c94cd7c08a9da2..00dcdcae88cab1cf7e4541fe42f828f2df5c6fb8 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -272,7 +272,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
-    iNext. eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
+    iNext. iApply (internal_eq_rewrite_contractive with "[Heq] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
   - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
     iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
@@ -280,7 +280,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
-    iNext. eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
+    iNext. iApply (internal_eq_rewrite_contractive with "[Heq] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
 Qed.
 
@@ -297,14 +297,14 @@ Proof.
     iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
       as (γ ?) "[#Hslice Hbox]"; first done.
     iExists γ. iIntros "{$% $#} !>". iNext.
-    eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
+    iApply (internal_eq_rewrite_contractive with "[Heq1 Heq2] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
   - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
     iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
     { by simplify_map_eq. }
     iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
     iExists γ. iIntros "{$% $#} !>". iNext.
-    eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
+    iApply (internal_eq_rewrite_contractive with "[Heq1 Heq2] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
 Qed.
 End box.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 332f7c77d9b918792781be28718ac06c879aea8a..0ce3e275ffa556b1bde0f10f200832fd051a744b 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -80,6 +80,25 @@ Qed.
 Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
 Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
 
+Lemma fupd_plain' E1 E2 E2' P Q `{!Plain P} :
+  E1 ⊆ E2 →
+  (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+Proof.
+  iIntros ((E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
+  rewrite fupd_eq /fupd_def ownE_op //. iIntros "H".
+  iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
+  iAssert (â—‡ P)%I as "#HP".
+  { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
+  iMod "HP". iFrame. auto.
+Qed.
+
+Lemma later_fupd_plain E P `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P.
+Proof.
+  rewrite fupd_eq /fupd_def. iIntros "HP [Hw HE]".
+  iAssert (â–· â—‡ P)%I with "[-]" as "#$"; last by iFrame.
+  iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
+Qed.
+
 (** * Derived rules *)
 Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@fupd Σ _ E1 E2).
 Proof. intros P Q; apply fupd_mono. Qed.
@@ -139,6 +158,13 @@ Proof.
   apply (big_opS_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
   intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
 Qed.
+
+Lemma fupd_plain E1 E2 P Q `{!Plain P} :
+  E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+Proof.
+  iIntros (HE) "HQP HQ". iApply (fupd_plain' _ _ E1 with "[HQP] HQ"); first done.
+  iIntros "?". iApply fupd_intro. by iApply "HQP".
+Qed.
 End fupd.
 
 (** Proofmode class instances *)
@@ -212,7 +238,7 @@ Section proofmode_classes.
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 End proofmode_classes.
 
-Hint Extern 2 (coq_tactics.of_envs _ ⊢ |={_}=> _) => iModIntro.
+Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.
 
 (** Fancy updates that take a step. *)
 
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 4cacc5c4f08e4201fede4673baf058ad1386f4fe..044318f2571ff40eac0f2bbf7e574a894d2da12e 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -151,6 +151,5 @@ End iProp_solution.
 Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
   iProp_unfold P ≡ iProp_unfold Q ⊢ (P ≡ Q : iProp Σ).
 Proof.
-  rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
-  apply: bi.f_equiv.
+  rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: bi.f_equiv.
 Qed.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 4ab1fd0292e1a33ace0493e7e49f329f32a06329..1de5366118a00520376bde214499435978b94ed6 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -44,7 +44,6 @@ Section saved_prop.
     assert (∀ z, G2 (G1 z) ≡ z) as help.
     { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
       apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
-    rewrite -{2}[x]help -{2}[y]help. apply later_mono.
-    apply f_equiv. solve_proper.
+    rewrite -{2}[x]help -{2}[y]help. apply later_mono, f_equiv, _.
   Qed.
 End saved_prop.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index 0347eeaa9af97aaf970b44d1fe9763d6d5d53249..dc86a510c440a9d8a9b9965a44ced3295f48d0d0 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import proofmode_classes.
 Import uPred.
 Import bi.
 
-Hint Extern 1 (coq_tactics.of_envs _ ⊢ |==> _) => iModIntro.
+Hint Extern 1 (coq_tactics.envs_entails _ (|==> _)) => iModIntro.
 
 Section class_instances.
 Context {M : ucmraT}.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 59a60e763b1ce570aa3aeec17c3b6c42b00eb50a..aba95a69c699e02f77b5ec326ad120e8521a75de 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -842,6 +842,3 @@ Section gmultiset.
 End gmultiset.
 End sbi_big_op.
 End bi.
-
-Hint Resolve bi.big_sepL_nil' bi.big_sepM_empty'
-  bi.big_sepS_empty' bi.big_sepMS_empty' | 0.
diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index e9b2f14e27c53a0b43c783557fff6579342aa78b..e2ff927401495b9351a4d3dfacd3d5ca4af41d44 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1741,9 +1741,9 @@ Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
+(* Not an instance, see the bottom of this file *)
 Lemma plain_persistent P : Plain P → Persistent P.
 Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
-Hint Immediate plain_persistent.
 
 (* Properties of persistent propositions *)
 Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ bi_persistently P.
@@ -1925,6 +1925,12 @@ Global Instance later_proper' :
   Proper ((⊣⊢) ==> (⊣⊢)) (@bi_later PROP) := ne_proper _.
 
 (* Equality *)
+Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → PROP)
+  {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+Proof.
+  rewrite later_eq_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
+  by apply internal_eq_rewrite.
+Qed.
 Lemma internal_eq_rewrite_contractive' {A : ofeT} a b (Ψ : A → PROP) P
   {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
@@ -2113,8 +2119,18 @@ Proof.
   - rewrite sep_or_r !sep_or_l {1}(later_intro P) {1}(later_intro Q).
     rewrite -!later_sep !left_absorb right_absorb. auto.
 Qed.
-Lemma except_0_forall_1 {A} (Φ : A → PROP) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
-Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
+Lemma except_0_forall {A} (Φ : A → PROP) : ◇ (∀ a, Φ a) ⊣⊢ ∀ a, ◇ Φ a.
+Proof.
+  apply (anti_symm _).
+  { apply forall_intro=> a. by rewrite (forall_elim a). }
+  trans (▷ (∀ a : A, Φ a) ∧ (∀ a : A, ◇ Φ a))%I.
+  { apply and_intro, reflexivity. rewrite later_forall. apply forall_mono=> a.
+    apply or_elim; auto using later_intro. }
+  rewrite later_false_em and_or_r. apply or_elim.
+  { rewrite and_elim_l. apply or_intro_l. }
+  apply or_intro_r', forall_intro=> a. rewrite !(forall_elim a).
+  by rewrite and_or_l impl_elim_l and_elim_r idemp.
+Qed.
 Lemma except_0_exist_2 {A} (Φ : A → PROP) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
 Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
 Lemma except_0_exist `{Inhabited A} (Φ : A → PROP) :
@@ -2157,6 +2173,13 @@ Proof.
   by apply and_mono, except_0_intro.
 Qed.
 
+Global Instance except_0_plain P : Plain P → Plain (◇ P).
+Proof. rewrite /bi_except_0; apply _. Qed.
+Global Instance except_0_persistent P : Persistent P → Persistent (◇ P).
+Proof. rewrite /bi_except_0; apply _. Qed.
+Global Instance except_0_absorbing P : Absorbing P → Absorbing (◇ P).
+Proof. rewrite /bi_except_0; apply _. Qed.
+
 (* Timeless instances *)
 Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
 Proof. solve_proper. Qed.
@@ -2198,11 +2221,8 @@ Qed.
 Global Instance forall_timeless {A} (Ψ : A → PROP) :
   (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
 Proof.
-  rewrite /Timeless=> HQ. rewrite later_false_em.
-  apply or_mono; first done. apply forall_intro=> x.
-  rewrite -(löb (Ψ x)); apply impl_intro_l.
-  rewrite HQ /bi_except_0 !and_or_r. apply or_elim; last auto.
-  by rewrite impl_elim_r (forall_elim x).
+  rewrite /Timeless=> HQ. rewrite except_0_forall later_forall.
+  apply forall_mono; auto.
 Qed.
 Global Instance exist_timeless {A} (Ψ : A → PROP) :
   (∀ x, Timeless (Ψ x)) → Timeless (∃ x, Ψ x).
@@ -2297,3 +2317,12 @@ Global Instance bi_except_0_sep_entails_homomorphism :
 Proof. split; try apply _. apply except_0_intro. Qed.
 End sbi_derived.
 End bi.
+
+(* When declared as an actual instance, [plain_persistent] will cause
+failing proof searches to take exponential time, as Coq will try to
+apply it the instance at any node in the proof search tree.
+
+To avoid that, we declare it using a [Hint Immediate], so that it will
+only be used at the leaves of the proof search tree, i.e. when the
+premise of the hint can be derived from just the current context. *)
+Hint Immediate bi.plain_persistent : typeclass_instances.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 6acb7414fb136c4bde0dfd8799dbbec381febc9a..e3fd5407518ba00c02e012b2e09cb1bae211f8ed 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -109,14 +109,6 @@ Fixpoint to_val (e : expr) : option val :=
   | _ => None
   end.
 
-Class AsRec (e : expr) (f x : binder) (erec : expr) :=
-  as_rec : e = Rec f x erec.
-
-Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
-Instance AsRec_rec_locked_val v f x e :
-  AsRec (of_val v) f x e → AsRec (of_val (locked v)) f x e.
-Proof. by unlock. Qed.
-
 (** The state: heaps of vals. *)
 Definition state := gmap loc val.
 
@@ -420,7 +412,7 @@ Lemma is_closed_of_val X v : is_closed X (of_val v).
 Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
 
 Lemma is_closed_to_val X e v : to_val e = Some v → is_closed X e.
-Proof. intros Hev; rewrite -(of_to_val e v Hev); apply is_closed_of_val. Qed.
+Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
 
 Lemma is_closed_subst X e x es :
   is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e).
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 9b597d4861f2bc8e73e2e31a33ebe9e6046f93a4..2e19c690d591b05767a33e19ef1bb1a56d381b10 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -83,16 +83,21 @@ Qed.
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
 Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pure_exec :=
-  repeat lazymatch goal with
-  | H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H
-  | H: AsRec _ _ _ _ |- _ => rewrite H; clear H
-  end;
+  unfold IntoVal, AsVal in *; subst;
+  repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
   apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
 
-Global Instance pure_rec f x (erec e1 e2 : expr) (v2 : val)
-    `{!IntoVal e2 v2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
+Class AsRec (e : expr) (f x : binder) (erec : expr) :=
+  as_rec : e = Rec f x erec.
+Global Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
+Global Instance AsRec_rec_locked_val v f x e :
+  AsRec (of_val v) f x e → AsRec (of_val (locked v)) f x e.
+Proof. by unlock. Qed.
+
+Global Instance pure_rec f x (erec e1 e2 : expr)
+    `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
   PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
-Proof. solve_pure_exec. Qed.
+Proof. unfold AsRec in *; solve_pure_exec. Qed.
 
 Global Instance pure_unop op e v v' `{!IntoVal e v} :
   PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
@@ -110,11 +115,11 @@ Global Instance pure_if_false e1 e2 :
   PureExec True (If (Lit (LitBool false)) e1 e2) e2.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_fst e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
+Global Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
   PureExec True (Fst (Pair e1 e2)) e1.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_snd e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
+Global Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
   PureExec True (Snd (Pair e1 e2)) e2.
 Proof. solve_pure_exec. Qed.
 
@@ -128,7 +133,7 @@ Proof. solve_pure_exec. Qed.
 
 (** Heap *)
 Lemma wp_alloc E e v :
-  to_val e = Some v →
+  IntoVal e v →
   {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
@@ -149,7 +154,7 @@ Proof.
 Qed.
 
 Lemma wp_store E l v' e v :
-  to_val e = Some v →
+  IntoVal e v →
   {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) ">Hl HΦ".
@@ -160,12 +165,12 @@ Proof.
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
-  to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
+Lemma wp_cas_fail E l q v' e1 v1 e2 :
+  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
   {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
   {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
 Proof.
-  iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
+  iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
@@ -173,7 +178,7 @@ Proof.
 Qed.
 
 Lemma wp_cas_suc E l e1 v1 e2 v2 :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  IntoVal e1 v1 → IntoVal e2 v2 →
   {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
   {{{ RET LitV (LitBool true); l ↦ v2 }}}.
 Proof.
@@ -184,23 +189,4 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
-
-(** Proof rules for derived constructs *)
-Lemma wp_seq E e1 e2 Φ :
-  is_Some (to_val e1) → Closed [] e2 →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?). rewrite -wp_pure_step_later; by eauto. Qed.
-
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
-Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
-
-Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
-  is_Some (to_val e0) → Closed (x1 :b: []) e1 →
-  ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
-
-Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
-  is_Some (to_val e0) → Closed (x2 :b: []) e2 →
-  ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
 End lifting.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index bd962e4958db116aa973787729219ac58440897a..b6ad39440274acac6393a49f191cf884afaf9f00 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -9,20 +9,25 @@ Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
   IntoLaterNEnvs 1 Δ Δ' →
-  (Δ' ⊢ WP fill K e2 @ E {{ Φ }}) →
-  (Δ ⊢ WP fill K e1 @ E {{ Φ }}).
+  envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
 Proof.
-  intros ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
   by rewrite -ectx_lifting.wp_ectx_bind_inv.
 Qed.
 
-Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
+Lemma tac_wp_value `{heapG Σ} Δ E Φ e v :
+  IntoVal e v →
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
+Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
+
+Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
 
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
     [simpl; apply _                 (* PureExec *)
@@ -47,19 +52,23 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
 Tactic Notation "wp_case" := wp_pure (Case _ _ _).
 Tactic Notation "wp_match" := wp_case; wp_let.
 
+Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e :
+  envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
+  envs_entails Δ (WP fill K e @ E {{ Φ }}).
+Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.
+
 Ltac wp_bind_core K :=
   lazymatch eval hnf in K with
   | [] => idtac
-  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
+  | _ => apply (tac_wp_bind K); simpl
   end.
 
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match e' with
-    | efoc => unify e' efoc; wp_bind_core K
-    end) || fail "wp_bind: cannot find" efoc "in" e
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
+    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
+    || fail "wp_bind: cannot find" efoc "in" e
   | _ => fail "wp_bind: not a 'wp'"
   end.
 
@@ -75,10 +84,11 @@ Lemma tac_wp_alloc Δ Δ' E j K e v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    (Δ'' ⊢ WP fill K (Lit (LitLoc l)) @ E {{ Φ }})) →
-  Δ ⊢ WP fill K (Alloc e) @ E {{ Φ }}.
+    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ E {{ Φ }})) →
+  envs_entails Δ (WP fill K (Alloc e) @ E {{ Φ }}).
 Proof.
-  intros ?? HΔ. rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
+  rewrite /envs_entails=> ?? HΔ.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
@@ -87,10 +97,11 @@ Qed.
 Lemma tac_wp_load Δ Δ' E i K l q v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  (Δ' ⊢ WP fill K (of_val v) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}.
+  envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}).
 Proof.
-  intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
+  rewrite /envs_entails=> ???.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -100,22 +111,24 @@ Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  (Δ'' ⊢ WP fill K (Lit LitUnit) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}.
+  envs_entails Δ'' (WP fill K (Lit LitUnit) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}).
 Proof.
-  intros. rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
+  rewrite /envs_entails=> ?????.
+  rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 v2 Φ :
-  IntoVal e1 v1 → IntoVal e2 v2 →
+Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 Φ :
+  IntoVal e1 v1 → AsVal e2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
-  (Δ' ⊢ WP fill K (Lit (LitBool false)) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}.
+  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
 Proof.
-  intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
+  rewrite /envs_entails=> ??????.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -125,10 +138,11 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  (Δ'' ⊢ WP fill K (Lit (LitBool true)) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}.
+  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
 Proof.
-  intros; subst. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
+  rewrite /envs_entails=> ???????; subst.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -137,7 +151,7 @@ End heap.
 Tactic Notation "wp_apply" open_constr(lem) :=
   iPoseProofCore lem as false true (fun H =>
     lazymatch goal with
-    | |- _ ⊢ wp ?E ?e ?Q =>
+    | |- envs_entails _ (wp ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
         wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
       lazymatch iTypeOf H with
@@ -149,7 +163,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_alloc _ _ _ H K); [apply _|..])
@@ -168,7 +182,7 @@ Tactic Notation "wp_alloc" ident(l) :=
 Tactic Notation "wp_load" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K))
       |fail 1 "wp_load: cannot find 'Load' in" e];
@@ -182,7 +196,7 @@ Tactic Notation "wp_load" :=
 Tactic Notation "wp_store" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_store _ _ _ _ _ K); [apply _|..])
@@ -198,7 +212,7 @@ Tactic Notation "wp_store" :=
 Tactic Notation "wp_cas_fail" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_cas_fail _ _ _ _ K); [apply _|apply _|..])
@@ -214,7 +228,7 @@ Tactic Notation "wp_cas_fail" :=
 Tactic Notation "wp_cas_suc" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 37af82a7d7820a273a83f869cf901395f2f4b4e7..6d7e58eaeb58dc8545d7db837a8a1bad4c5171bc 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -114,7 +114,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
 Lemma is_closed_correct X e : is_closed X e → heap_lang.is_closed X (to_expr e).
 Proof.
   revert X.
-  induction e; naive_solver eauto using is_closed_of_val, is_closed_to_val, is_closed_weaken_nil.
+  induction e; naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
 Qed.
 
 (* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
@@ -172,10 +172,10 @@ Lemma to_expr_subst x er e :
   to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
 Proof.
   induction e; simpl; repeat case_decide;
-    f_equal; eauto using subst_is_closed_nil, is_closed_of_val, is_closed_to_val, eq_sym.
+    f_equal; eauto using subst_is_closed_nil, is_closed_to_val, eq_sym.
 Qed.
 
-Definition atomic (e : expr) :=
+Definition is_atomic (e : expr) :=
   match e with
   | Alloc e => bool_decide (is_Some (to_val e))
   | Load e => bool_decide (is_Some (to_val e))
@@ -187,7 +187,7 @@ Definition atomic (e : expr) :=
   | App (Rec _ _ (Lit _)) (Lit _) => true
   | _ => false
   end.
-Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
+Lemma is_atomic_correct e : is_atomic e → Atomic (to_expr e).
 Proof.
   intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef Hstep; simpl in *.
@@ -209,31 +209,29 @@ Ltac solve_closed :=
   end.
 Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
 
-Ltac solve_to_val :=
-  rewrite /IntoVal;
-  try match goal with
-  | |- context E [language.to_val ?e] =>
-     let X := context E [to_val e] in change X
-  end;
+Ltac solve_into_val :=
   match goal with
-  | |- to_val ?e = Some ?v =>
+  | |- IntoVal ?e ?v =>
      let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
      apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity
-  | |- is_Some (to_val ?e) =>
+  end.
+Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
+
+Ltac solve_as_val :=
+  match goal with
+  | |- AsVal ?e =>
      let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
      apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
-Hint Extern 10 (IntoVal _ _) => solve_to_val : typeclass_instances.
+Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with
-  | |- language.atomic ?e =>
-     let e' := W.of_expr e in change (language.atomic (W.to_expr e'));
-     apply W.atomic_correct; vm_compute; exact I
+  | |- Atomic ?e =>
+     let e' := W.of_expr e in change (Atomic (W.to_expr e'));
+     apply W.is_atomic_correct; vm_compute; exact I
   end.
-Hint Extern 10 (language.atomic _) => solve_atomic.
-(* For the side-condition of elim_upd_fupd_wp_atomic *)
-Hint Extern 10 (language.atomic _) => solve_atomic : typeclass_instances.
+Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances.
 
 (** Substitution *)
 Ltac simpl_subst :=
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 65da78ed1f05df4ba649a543d4b2d4b6a7910087..e9e92ab5ded233a35c1e720db1ae74327256c4a2 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -118,7 +118,7 @@ Section ectx_language.
   Lemma ectx_language_atomic e :
     (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
     sub_values e →
-    atomic e.
+    Atomic e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index e00826d27961fa179ecc330e4942a7ca78f88ef9..11d2e689d2d0f1414e30cc9a7b9e990c002f5586 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -58,7 +58,7 @@ Proof.
 Qed.
 
 Lemma ht_atomic E1 E2 P P' Φ Φ' e :
-  atomic e →
+  Atomic e →
   (P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊢ {{ P }} e @ E1 {{ Φ }}.
 Proof.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 88c82f8eb78b43b8d7b951ff497cf450c0b69722..8189151d5739006bfd683cd7dae9844bead6bf35 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -52,8 +52,21 @@ Section language.
   Definition irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ e' σ' efs, ¬prim_step e σ e' σ' efs.
 
-  Definition atomic (e : expr Λ) : Prop :=
-    ∀ σ e' σ' efs, prim_step e σ e' σ' efs → irreducible e' σ'.
+  (* This (weak) form of atomicity is enough to open invariants when WP ensures
+     safety, i.e., programs never can get stuck.  We have an example in
+     lambdaRust of an expression that is atomic in this sense, but not in the
+     stronger sense defined below, and we have to be able to open invariants
+     around that expression.  See `CasStuckS` in
+     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v). *)
+  Class Atomic (e : expr Λ) : Prop :=
+    atomic σ e' σ' efs : prim_step e σ e' σ' efs → irreducible e' σ'.
+
+  (* To open invariants with a WP that does not ensure safety, we need a
+     stronger form of atomicity.  With the above definition, in case `e` reduces
+     to a stuck non-value, there is no proof that the invariants have been
+     established again. *)
+  Class StronglyAtomic (e : expr Λ) : Prop :=
+    strongly_atomic σ e' σ' efs : prim_step e σ e' σ' efs → is_Some (to_val e').
 
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
@@ -74,6 +87,9 @@ Section language.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
+  Lemma strongly_atomic_atomic e : StronglyAtomic e → Atomic e.
+  Proof. unfold StronglyAtomic, Atomic. eauto using val_irreducible. Qed.
+
   Lemma reducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.
   Proof.
@@ -109,4 +125,13 @@ Section language.
   (* This is a family of frequent assumptions for PureExec *)
   Class IntoVal (e : expr Λ) (v : val Λ) :=
     into_val : to_val e = Some v.
+
+  Class AsVal (e : expr Λ) := as_val : is_Some (to_val e).
+  (* There is no instance [IntoVal → AsVal] as often one can solve [AsVal] more
+  efficiently since no witness has to be computed. *)
+  Global Instance as_vals_of_val vs : TCForall AsVal (of_val <$> vs).
+  Proof.
+    apply TCForall_Forall, Forall_fmap, Forall_true=> v.
+    rewrite /AsVal /= to_of_val; eauto.
+  Qed.
 End language.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 92842e1c7095a40e9344dce8f79267531a8e6a6b..08a7649d86d256e976d3ba1fe951b4a32d57f970 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -146,7 +146,7 @@ Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
 Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
 
 Lemma wp_atomic E1 E2 e Φ :
-  atomic e →
+  Atomic e →
   (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
 Proof.
   iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
@@ -284,10 +284,8 @@ Section proofmode_classes.
 
   (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
   Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
-    atomic e →
+    Atomic e →
     ElimModal (|={E1,E2}=> P) P
             (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
 End proofmode_classes.
-
-Hint Extern 0 (atomic _) => assumption : typeclass_instances.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 39d4ec51568bd584701d3c025ba804a891332543..90f3c2737e6be751a00f3d2b44ead5b87e7fe7b5 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -7,23 +7,6 @@ Section bi_instances.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 
-(* IntoInternalEq *)
-Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
-  @IntoInternalEq PROP A (x ≡ y) x y.
-Proof. by rewrite /IntoInternalEq. Qed.
-Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
-  IntoInternalEq P x y → IntoInternalEq (bi_affinely P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
-Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
-  IntoInternalEq P x y → IntoInternalEq (▲ P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
-Global Instance into_internal_eq_plainly {A : ofeT} (x y : A) P :
-  IntoInternalEq P x y → IntoInternalEq (bi_plainly P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
-Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
-  IntoInternalEq P x y → IntoInternalEq (bi_persistently P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
-
 (* FromAffinely *)
 Global Instance from_affinely_affine P : Affine P → FromAffinely P P.
 Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
@@ -179,6 +162,23 @@ Proof. by rewrite /FromPure affine_affinely. Qed.
 Global Instance from_pure_absorbingly P φ : FromPure P φ → FromPure (▲ P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
 
+(* IntoInternalEq *)
+Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
+  @IntoInternalEq PROP A (x ≡ y) x y.
+Proof. by rewrite /IntoInternalEq. Qed.
+Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (bi_affinely P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
+Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (▲ P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
+Global Instance into_internal_eq_plainly {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (bi_plainly P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
+Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (bi_persistently P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
+
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
   IntoPersistent true P Q → IntoPersistent p (bi_persistently P) Q | 0.
@@ -1013,11 +1013,17 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
 Global Instance into_forall_later {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (▷ P) (λ a, ▷ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
+Global Instance into_forall_except_0 {A} P (Φ : A → PROP) :
+  IntoForall P Φ → IntoForall (◇ P) (λ a, ◇ (Φ a))%I.
+Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
 
 (* FromForall *)
 Global Instance from_forall_later {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (▷ P)%I (λ a, ▷ (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
+Global Instance from_forall_except_0 {A} P (Φ : A → PROP) :
+  FromForall P Φ → FromForall (◇ P)%I (λ a, ◇ (Φ a))%I.
+Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed.
 
 (* IsExcept0 *)
 Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 1d5f1139377c87c26fdd02d1635ec18a42aded06..8f959e4e1839672297dc374ef75ed967a0a836cd 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -49,6 +49,12 @@ Arguments FromPure {_} _%I _%type_scope : simpl never.
 Arguments from_pure {_} _%I _%type_scope {_}.
 Hint Mode FromPure + ! - : typeclass_instances.
 
+Class IntoInternalEq {PROP : bi} {A : ofeT} (P : PROP) (x y : A) :=
+  into_internal_eq : P ⊢ x ≡ y.
+Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.
+Arguments into_internal_eq {_ _} _%I _%type_scope _%type_scope {_}.
+Hint Mode IntoInternalEq + - ! - - : typeclass_instances.
+
 Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
   into_persistent : bi_persistently_if p P ⊢ bi_persistently Q.
 Arguments IntoPersistent {_} _ _%I _%I : simpl never.
@@ -74,12 +80,6 @@ Arguments into_absorbingly {_} _%I _%I {_}.
 Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
 Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
 
-Class IntoInternalEq {PROP : bi} {A : ofeT} (P : PROP) (x y : A) :=
-  into_internal_eq : P ⊢ x ≡ y.
-Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.
-Arguments into_internal_eq {_ _} _%I _%type_scope _%type_scope {_}.
-Hint Mode IntoInternalEq + - ! - - : typeclass_instances.
-
 (*
 Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
 
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 66fc81fb1bc579524ee8599cf3020fce711d3887..f0c27d5c8a42813f97f27d47a8ab7c91cc62109a 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -21,11 +21,17 @@ Record envs_wf {PROP} (Δ : envs PROP) := {
   envs_disjoint i : env_persistent Δ !! i = None ∨ env_spatial Δ !! i = None
 }.
 
-Coercion of_envs {PROP} (Δ : envs PROP) : PROP :=
+Definition of_envs {PROP} (Δ : envs PROP) : PROP :=
   (⌜envs_wf Δ⌝ ∧ □ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
 Instance: Params (@of_envs) 1.
 Arguments of_envs : simpl never.
 
+Definition envs_entails {PROP} (Δ : envs PROP) (Q : PROP) : Prop :=
+  of_envs Δ ⊢ Q.
+Arguments envs_entails {_} _ _%I : simpl never.
+Typeclasses Opaque envs_entails.
+Instance: Params (@envs_entails) 1.
+
 Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs 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)
@@ -139,7 +145,8 @@ Proof.
 Qed.
 
 Lemma envs_lookup_sound Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ envs_delete i p Δ.
+  envs_lookup i Δ = Some (p,P) →
+  of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete i p Δ).
 Proof.
   rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -153,7 +160,7 @@ Proof.
     rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
 Qed.
 Lemma envs_lookup_persistent_sound Δ i P :
-  envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ∗ Δ.
+  envs_lookup i Δ = Some (true,P) → of_envs Δ ⊢ □ P ∗ of_envs Δ.
 Proof.
   intros. rewrite -persistently_and_affinely_sep_l. apply and_intro; last done.
   rewrite envs_lookup_sound //; simpl.
@@ -161,7 +168,7 @@ Proof.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ (□?p P -∗ Δ).
+  envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ (□?p P -∗ of_envs Δ).
 Proof.
   rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -174,12 +181,12 @@ Proof.
 Qed.
 
 Lemma envs_lookup_delete_sound Δ Δ' i p P :
-  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ □?p P ∗ Δ'.
+  envs_lookup_delete i Δ = Some (p,P,Δ') → of_envs Δ ⊢ □?p P ∗ of_envs Δ'.
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
 
 Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
-  envs_lookup_delete_list js rp Δ = Some (p,Ps,Δ') →
-  Δ ⊢ □?p [∗] Ps ∗ Δ'.
+  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') →
+  of_envs Δ ⊢ □?p [∗] Ps ∗ of_envs Δ'.
 Proof.
   revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
   { by rewrite affinely_persistently_emp left_id. }
@@ -209,7 +216,7 @@ Proof.
 Qed.
 
 Lemma envs_snoc_sound Δ p i P :
-  envs_lookup i Δ = None → Δ ⊢ □?p P -∗ envs_snoc Δ p i P.
+  envs_lookup i Δ = None → of_envs Δ ⊢ □?p P -∗ of_envs (envs_snoc Δ p i P).
 Proof.
   rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
@@ -225,7 +232,8 @@ Proof.
 Qed.
 
 Lemma envs_app_sound Δ Δ' p Γ :
-  envs_app p Γ Δ = Some Δ' → Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ Δ'.
+  envs_app p Γ Δ = Some Δ' →
+  of_envs Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -248,12 +256,12 @@ Proof.
 Qed.
 
 Lemma envs_app_singleton_sound Δ Δ' p j Q :
-  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ⊢ □?p Q -∗ Δ'.
+  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → of_envs Δ ⊢ □?p Q -∗ of_envs Δ'.
 Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.
 
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
   envs_simple_replace i p Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ Δ'.
+  of_envs (envs_delete i p Δ) ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
   apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -277,25 +285,25 @@ Qed.
 
 Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
   envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
-  envs_delete i p Δ ⊢ □?p Q -∗ Δ'.
+  of_envs (envs_delete i p Δ) ⊢ □?p Q -∗ of_envs Δ'.
 Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.
 
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ Δ').
+  of_envs Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
 Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
   envs_lookup i Δ = Some (p,P) →
   envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
-  Δ ⊢ □?p P ∗ (□?p Q -∗ Δ').
+  of_envs Δ ⊢ □?p P ∗ (□?p Q -∗ of_envs Δ').
 Proof.
   intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
 Qed.
 
 Lemma envs_replace_sound' Δ Δ' i p q Γ :
   envs_replace i p q Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ Δ'.
+  of_envs (envs_delete i p Δ) ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
@@ -304,18 +312,18 @@ Qed.
 
 Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
   envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
-  envs_delete i p Δ ⊢ □?q Q -∗ Δ'.
+  of_envs (envs_delete i p Δ) ⊢ □?q Q -∗ of_envs Δ'.
 Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.
 
 Lemma envs_replace_sound Δ Δ' i p q P Γ :
   envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
-  Δ ⊢ □?p P ∗ ((if q then □ [∧] Γ else [∗] Γ) -∗ Δ').
+  of_envs Δ ⊢ □?p P ∗ ((if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
 
 Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
   envs_lookup i Δ = Some (p,P) →
   envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
-  Δ ⊢ □?p P ∗ (□?q Q -∗ Δ').
+  of_envs Δ ⊢ □?p P ∗ (□?q Q -∗ of_envs Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.
 
 Lemma envs_lookup_envs_clear_spatial Δ j :
@@ -328,7 +336,7 @@ Proof.
 Qed.
 
 Lemma envs_clear_spatial_sound Δ :
-  Δ ⊢ envs_clear_spatial Δ ∗ [∗] env_spatial Δ.
+  of_envs Δ ⊢ of_envs (envs_clear_spatial Δ) ∗ [∗] env_spatial Δ.
 Proof.
   rewrite /of_envs /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
   rewrite right_id -persistent_and_sep_assoc. apply and_intro; [|done].
@@ -336,7 +344,7 @@ Proof.
 Qed.
 
 Lemma env_spatial_is_nil_affinely_persistently Δ :
-  env_spatial_is_nil Δ = true → Δ ⊢ □ Δ.
+  env_spatial_is_nil Δ = true → of_envs Δ ⊢ □ of_envs Δ.
 Proof.
   intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
   rewrite !right_id {1}affinely_and_r persistently_and.
@@ -364,7 +372,7 @@ Qed.
 Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
   (∀ j P, envs_lookup j Δ1 = Some (false, P) → envs_lookup j Δ2 = None) →
   envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') →
-  Δ1 ∗ Δ2 ⊢ Δ1' ∗ Δ2'.
+  of_envs Δ1 ∗ of_envs Δ2 ⊢ of_envs Δ1' ∗ of_envs Δ2'.
 Proof.
   revert Δ1 Δ2 Δ1' Δ2'.
   induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|].
@@ -381,9 +389,9 @@ Proof.
   rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
 Qed.
 Lemma envs_split_sound Δ d js Δ1 Δ2 :
-  envs_split d js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ∗ Δ2.
+  envs_split d js Δ = Some (Δ1,Δ2) → of_envs Δ ⊢ of_envs Δ1 ∗ of_envs Δ2.
 Proof.
-  rewrite /envs_split=> ?. rewrite -(idemp bi_and Δ).
+  rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)).
   rewrite {2}envs_clear_spatial_sound.
   rewrite (env_spatial_is_nil_affinely_persistently (envs_clear_spatial _)) //.
   rewrite -persistently_and_affinely_sep_l.
@@ -424,12 +432,19 @@ Proof.
   intros Δ1 Δ2 HΔ; apply (anti_symm (⊢)); apply of_envs_mono;
     eapply (envs_Forall2_impl (⊣⊢)); [| |symmetry|]; eauto using equiv_entails.
 Qed.
-Global Instance Envs_mono (R : relation PROP) :
+Global Instance Envs_proper (R : relation PROP) :
   Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs PROP).
 Proof. by constructor. Qed.
 
+Global Instance envs_entails_proper :
+  Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢) ==> iff) (@envs_entails PROP).
+Proof. solve_proper. Qed.
+Global Instance envs_entails_flip_mono :
+  Proper (envs_Forall2 (⊢) ==> flip (⊢) ==> flip impl) (@envs_entails PROP).
+Proof. rewrite /envs_entails=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
+
 (** * Adequacy *)
-Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → P.
+Lemma tac_adequate P : envs_entails (Envs Enil Enil) P → P.
 Proof.
   intros <-. rewrite /of_envs /= persistently_True_emp affinely_persistently_emp left_id.
   apply and_intro=> //. apply pure_intro; repeat constructor.
@@ -451,15 +466,15 @@ Instance affine_env_spatial Δ :
   AffineEnv (env_spatial Δ) → Affine ([∗] env_spatial Δ).
 Proof. intros H. induction H; simpl; apply _. Qed.
 
-Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → Δ ⊢ emp.
-Proof. intros. by rewrite (affine Δ). Qed.
+Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → of_envs Δ ⊢ emp.
+Proof. intros. by rewrite (affine (of_envs Δ)). Qed.
 
 Lemma tac_assumption Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
   FromAssumption p P Q →
   (if env_spatial_is_nil Δ' then TCTrue
    else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
-  Δ ⊢ Q.
+  of_envs Δ ⊢ Q.
 Proof.
   intros ?? H. rewrite envs_lookup_delete_sound //.
   destruct (env_spatial_is_nil Δ') eqn:?.
@@ -470,46 +485,48 @@ Qed.
 Lemma tac_rename Δ Δ' i j p P Q :
   envs_lookup i Δ = Some (p,P) →
   envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q →
+  envs_entails Δ Q.
 Proof.
-  intros. rewrite envs_simple_replace_singleton_sound //.
+  rewrite /envs_entails=> ?? <-. rewrite envs_simple_replace_singleton_sound //.
   by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_clear Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
-  (Δ' ⊢ Q) →
-  Δ ⊢ Q.
+  (envs_entails Δ' Q) →
+  envs_entails Δ Q.
 Proof.
-  intros ? Hp HQ. rewrite envs_lookup_delete_sound //.
-  destruct p; by rewrite /= HQ sep_elim_r.
+  rewrite /envs_entails=> ?? HQ. rewrite envs_lookup_delete_sound //.
+  by destruct p; rewrite /= HQ sep_elim_r.
 Qed.
 
 (** * False *)
-Lemma tac_ex_falso Δ Q : (Δ ⊢ False) → Δ ⊢ Q.
-Proof. by rewrite -(False_elim Q). Qed.
+Lemma tac_ex_falso Δ Q : envs_entails Δ False → envs_entails Δ Q.
+Proof. by rewrite /envs_entails -(False_elim Q). Qed.
 
 Lemma tac_false_destruct Δ i p P Q :
   envs_lookup i Δ = Some (p,P) →
   P = False%I →
-  Δ ⊢ Q.
+  envs_entails Δ Q.
 Proof.
-  intros ? ->. rewrite envs_lookup_sound //; simpl.
+  rewrite /envs_entails => ??. subst. rewrite envs_lookup_sound //; simpl.
   by rewrite affinely_persistently_if_elim sep_elim_l False_elim.
 Qed.
 
 (** * Pure *)
-Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ → φ → Δ ⊢ Q.
-Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
+Lemma tac_pure_intro Δ Q φ : FromPure Q φ → φ → envs_entails Δ Q.
+Proof. intros ??. rewrite /envs_entails -(from_pure Q). by apply pure_intro. Qed.
 
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') →
   IntoPure P φ →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
-  (φ → Δ' ⊢ Q) → Δ ⊢ Q.
+  (φ → envs_entails Δ' Q) → envs_entails Δ Q.
 Proof.
-  intros ?? HPQ HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
+  rewrite /envs_entails=> ?? HPQ HQ.
+  rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
   - rewrite (into_pure P) -persistently_and_affinely_sep_l persistently_pure.
     by apply pure_elim_l.
   - destruct HPQ.
@@ -519,8 +536,8 @@ Proof.
       rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 
-Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ⌜φ⌝ → Q) → (φ → Δ ⊢ Q).
-Proof. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
+Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → envs_entails Δ Q).
+Proof. rewrite /envs_entails. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
 (** * Persistence and plainness modalities *)
 Class IntoPlainEnv (Γ1 Γ2 : env PROP) := {
@@ -539,8 +556,8 @@ Global Instance into_plain_env_snoc_skip Γ1 Γ2 i P :
 Proof. intros [??]; constructor. by constructor. done. Qed.
 
 Lemma into_plain_env_sound Γ1 Γ2 :
-  IntoPlainEnv Γ1 Γ2 → (Envs Γ1 Enil) ⊢ bi_plainly (Envs Γ2 Enil).
-Proof .
+  IntoPlainEnv Γ1 Γ2 → of_envs (Envs Γ1 Enil) ⊢ bi_plainly $ of_envs $ Envs Γ2 Enil.
+Proof.
   intros [Hsub ?]. rewrite !of_envs_eq plainly_and plainly_pure /=. f_equiv.
   { f_equiv=>-[/= ???]. split; auto. by eapply env_subenv_wf. }
   rewrite !(right_id emp%I). trans (□ [∧] Γ2)%I.
@@ -572,10 +589,12 @@ Lemma tac_always_intro Δ Δ' a pe pl Q Q' :
   FromAlways a pe pl Q' Q →
   (if a then AffineEnv (env_spatial Δ') else TCTrue) →
   IntoAlwaysEnvs pe pl Δ' Δ →
-  (Δ ⊢ Q) → Δ' ⊢ Q'.
+  (envs_entails Δ Q) → envs_entails Δ' Q'.
 Proof.
-  intros ? Haffine [Hep Hes] HQ. rewrite -(from_always a pe pl Q') -HQ.
-  trans (bi_affinely_if a Δ'); [destruct a=>//; by apply: affinely_intro|f_equiv].
+  rewrite /envs_entails => ? Haffine [Hep Hes] HQ.
+  rewrite -(from_always a pe pl Q') -HQ.
+  trans (bi_affinely_if a (of_envs Δ'));
+    [destruct a=>//; by apply: affinely_intro|f_equiv].
   destruct pl; [|destruct pe].
   - rewrite (envs_clear_spatial_sound Δ') into_plain_env_sound sep_elim_l.
     destruct Δ as [Δ ?]. rewrite orb_true_r /= in Hes. rewrite Hes /=.
@@ -593,9 +612,9 @@ Lemma tac_persistent Δ Δ' i p P P' Q :
   IntoPersistent p P P' →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros ?? HPQ ? HQ. rewrite envs_replace_singleton_sound //; simpl.
+  rewrite /envs_entails=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
   destruct p; simpl.
   - by rewrite -(into_persistent _ P) /= wand_elim_r.
   - destruct HPQ.
@@ -608,16 +627,16 @@ Qed.
 
 (** * Implication and wand *)
 Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
-  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ∗ □?p Q ⊢ Δ'.
+  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → of_envs Δ ∗ □?p Q ⊢ of_envs Δ'.
 Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.
 
 Lemma tac_impl_intro Δ Δ' i P P' Q :
   (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
   envs_app false (Esnoc Enil i P') Δ = Some Δ' →
   FromAffinely P' P →
-  (Δ' ⊢ Q) → Δ ⊢ P → Q.
+  envs_entails Δ' Q → envs_entails Δ (P → Q).
 Proof.
-  intros ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
+  rewrite /envs_entails => ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
   - rewrite (env_spatial_is_nil_affinely_persistently Δ) //; simpl. apply impl_intro_l.
     rewrite envs_app_singleton_sound //; simpl.
     rewrite -(from_affinely P') -affinely_and_lr.
@@ -628,35 +647,39 @@ Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ P → Q.
+  envs_entails Δ' Q → envs_entails Δ (P → Q).
 Proof.
-  intros ?? <-. rewrite envs_app_singleton_sound //; simpl. apply impl_intro_l.
+  rewrite /envs_entails => ?? <-.
+  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
   rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
   by rewrite persistently_and_affinely_sep_l wand_elim_r.
 Qed.
 Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
-  (φ → Δ ⊢ ⌜ψ⌝) → Δ ⊢ ⌜φ → ψ⌝.
+  (φ → envs_entails Δ ⌜ψ⌝) → envs_entails Δ ⌜φ → ψ⌝.
 Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
-Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
+Lemma tac_impl_intro_pure Δ P φ Q :
+  IntoPure P φ → (φ → envs_entails Δ Q) → envs_entails Δ (P → Q).
 Proof.
   intros. apply impl_intro_l. rewrite (into_pure P). by apply pure_elim_l.
 Qed.
 
-Lemma tac_impl_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P → Q.
-Proof. intros. apply impl_intro_l. by rewrite and_elim_r. Qed.
+Lemma tac_impl_intro_drop Δ P Q : envs_entails Δ Q → envs_entails Δ (P → Q).
+Proof. rewrite /envs_entails=> ?. apply impl_intro_l. by rewrite and_elim_r. Qed.
 
 Lemma tac_wand_intro Δ Δ' i P Q :
-  envs_app false (Esnoc Enil i P) Δ = Some Δ' → (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
+  envs_app false (Esnoc Enil i P) Δ = Some Δ' →
+  envs_entails Δ' Q → envs_entails Δ (P -∗ Q).
 Proof.
-  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
+  rewrite /envs_entails=> ? HQ.
+  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
 Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
   TCOr (Affine P) (Absorbing Q) →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
+  envs_entails Δ' Q → envs_entails Δ (P -∗ Q).
 Proof.
-  intros ? HPQ ? HQ. rewrite envs_app_singleton_sound //; simpl.
+  rewrite /envs_entails => ? HPQ ? HQ. rewrite envs_app_singleton_sound //=.
   apply wand_intro_l. destruct HPQ.
   - rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
             (into_persistent _ P) wand_elim_r //.
@@ -667,7 +690,7 @@ Qed.
 Lemma tac_wand_intro_pure Δ P φ Q :
   IntoPure P φ →
   TCOr (Affine P) (Absorbing Q) →
-  (φ → Δ ⊢ Q) → Δ ⊢ P -∗ Q.
+  (φ → envs_entails Δ Q) → envs_entails Δ (P -∗ Q).
 Proof.
   intros ? HPQ HQ. apply wand_intro_l. destruct HPQ.
   - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
@@ -677,9 +700,11 @@ Proof.
 Qed.
 Lemma tac_wand_intro_drop Δ P Q :
   TCOr (Affine P) (Absorbing Q) →
-  (Δ ⊢ Q) →
-  Δ ⊢ P -∗ Q.
-Proof. intros HPQ ->. apply wand_intro_l. by rewrite sep_elim_r. Qed.
+  envs_entails Δ Q →
+  envs_entails Δ (P -∗ Q).
+Proof.
+  rewrite /envs_entails => HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
+Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
 but it is doing some work to keep the order of hypotheses preserved. *)
@@ -692,9 +717,9 @@ Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
   | false => envs_replace j q false (Esnoc Enil j P2) Δ'
              (* remove [i] and make [j] spatial *)
   end = Some Δ'' →
-  (Δ'' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ'' Q → envs_entails Δ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
   - rewrite envs_lookup_persistent_sound //.
     rewrite envs_simple_replace_singleton_sound //; simpl.
     rewrite -affinely_persistently_if_idemp -affinely_persistently_idemp into_wand /=.
@@ -712,9 +737,9 @@ Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
   ('(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
     Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
-  (Δ1 ⊢ P1') → (Δ2' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ1 P1' → envs_entails Δ2' Q → envs_entails Δ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
@@ -723,18 +748,18 @@ Proof.
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
-Lemma tac_unlock P Q : (P ⊢ Q) → P ⊢ locked Q.
+Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
 Proof. by unlock. Qed.
 
 Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
   IntoWand q false R P1 P2 →
   ElimModal P1' P1 Q Q →
-  (Δ' ⊢ P1' ∗ locked Q') →
+  envs_entails Δ' (P1' ∗ locked Q') →
   Q' = (P2 -∗ Q)%I →
-  Δ ⊢ Q.
+  envs_entails Δ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
   rewrite into_wand -{2}(elim_modal P1' P1 Q Q). cancel [P1'].
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
@@ -745,9 +770,9 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   IntoWand q true R P1 P2 →
   FromPure P1 φ →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
-  φ → (Δ' ⊢ Q) → Δ ⊢ Q.
+  φ → envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros. rewrite envs_simple_replace_singleton_sound //; simpl.
+  rewrite /envs_entails=> ????? <-. rewrite envs_simple_replace_singleton_sound //=.
   rewrite -affinely_persistently_if_idemp into_wand /= -(from_pure P1).
   rewrite pure_True // persistently_pure affinely_True_emp affinely_emp.
   by rewrite emp_wand wand_elim_r.
@@ -759,11 +784,11 @@ Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P1' P2 R Q :
   Persistent P1 →
   IntoAbsorbingly P1' P1 →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
-  (Δ' ⊢ P1') → (Δ'' ⊢ Q) → Δ ⊢ Q.
+  (envs_entails Δ' P1') → (envs_entails Δ'' Q) → envs_entails Δ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ???? HP1 <-.
+  rewrite /envs_entails => /envs_lookup_delete_Some [? ->] ???? HP1 <-.
   rewrite envs_lookup_sound //.
-  rewrite -(idemp bi_and (envs_delete _ _ _)).
+  rewrite -(idemp bi_and (of_envs (envs_delete _ _ _))).
   rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
   rewrite {1}HP1 (into_absorbingly P1') (persistent_persistently_2 P1).
   rewrite absorbingly_persistently persistently_and_affinely_sep_l assoc.
@@ -774,13 +799,13 @@ Qed.
 
 Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
   envs_lookup j Δ = Some (q,P) →
-  (Δ ⊢ ▲ R) →
+  envs_entails Δ (▲ R) →
   IntoPersistent false R R' →
   (if q then TCTrue else AffineBI PROP) →
   envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' →
-  (Δ'' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ'' Q → envs_entails Δ Q.
 Proof.
-  intros ? HR ? Hpos ? <-. rewrite -(idemp bi_and Δ) {1}HR.
+  rewrite /envs_entails => ? HR ? Hpos ? <-. rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
   rewrite envs_replace_singleton_sound //; destruct q; simpl.
   - by rewrite (_ : R = bi_persistently_if false R)%I // (into_persistent _ R)
       absorbingly_persistently sep_elim_r persistently_and_affinely_sep_l wand_elim_r.
@@ -790,32 +815,35 @@ Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
-  (Δ' ⊢ (if p then □ P else P) -∗ Q) → Δ ⊢ Q.
+  envs_entails Δ' ((if p then □ P else P)%I -∗ Q) →
+  envs_entails Δ Q.
 Proof.
-  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
+  rewrite /envs_entails => ? HQ. rewrite envs_lookup_delete_sound //=.
   rewrite HQ. destruct p; simpl; auto using wand_elim_r.
 Qed.
 
 Class IntoIH {PROP : bi} (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
-  into_ih : φ → Δ ⊢ Q.
-Global Instance into_ih_entails Δ Q : IntoIH (of_envs Δ ⊢ Q) Δ Q.
+  into_ih : φ → of_envs Δ ⊢ Q.
+Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
 Proof. by rewrite /IntoIH. Qed.
 Global Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
   (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x)%I | 2.
 Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
 Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
   IntoIH φ Δ Q → IntoIH (ψ → φ) Δ (⌜ψ⌝ → Q)%I | 1.
-Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
+Proof.
+  rewrite /IntoIH /envs_entails=> HΔ ?. apply impl_intro_l, pure_elim_l. auto.
+Qed.
 
 Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
   IntoIH φ Δ P →
   env_spatial_is_nil Δ = true →
-  (of_envs Δ ⊢ bi_persistently P → Q) →
-  (of_envs Δ ⊢ Q).
+  envs_entails Δ (bi_persistently P → Q) →
+  envs_entails Δ Q.
 Proof.
-  rewrite /IntoIH. intros HP ? HPQ.
+  rewrite /IntoIH /envs_entails. intros HP ? HPQ.
   rewrite (env_spatial_is_nil_affinely_persistently Δ) //.
-  rewrite -(idemp bi_and (□ Δ)%I) {1}HP // HPQ.
+  rewrite -(idemp bi_and (□ (of_envs Δ))%I) {1}HP // HPQ.
   by rewrite -{1}persistently_idemp !affinely_persistently_elim impl_elim_r.
 Qed.
 
@@ -823,9 +851,9 @@ Lemma tac_assert Δ Δ1 Δ2 Δ2' neg js j P P' Q :
   ElimModal P' P Q Q →
   envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
-  (Δ1 ⊢ P') → (Δ2' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ1 P' → envs_entails Δ2' Q → envs_entails Δ Q.
 Proof.
-  intros ??? HP HQ. rewrite envs_split_sound //.
+  rewrite /envs_entails=>??? HP HQ. rewrite envs_split_sound //.
   rewrite (envs_app_singleton_sound Δ2) //; simpl. by rewrite HP HQ.
 Qed.
 
@@ -834,9 +862,10 @@ Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' neg js j P P' Q :
   Persistent P →
   FromAffinely P' P →
   envs_app false (Esnoc Enil j P') Δ = Some Δ' →
-  (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ1 P → envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros ???? HP <-. rewrite -(idemp bi_and Δ) {1}envs_split_sound //.
+  rewrite /envs_entails => ???? HP <-.
+  rewrite -(idemp bi_and (of_envs Δ)) {1}envs_split_sound //.
   rewrite HP. rewrite (persistent_persistently_2 P) sep_elim_l.
   rewrite persistently_and_affinely_sep_l -affinely_idemp.
   rewrite affinely_persistently_elim from_affinely envs_app_singleton_sound //=.
@@ -847,9 +876,9 @@ Lemma tac_assert_pure Δ Δ' j P P' φ Q :
   FromPure P φ →
   FromAffinely P' P →
   envs_app false (Esnoc Enil j P') Δ = Some Δ' →
-  φ → (Δ' ⊢ Q) → Δ ⊢ Q.
+  φ → envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros ???? <-. rewrite envs_app_singleton_sound //; simpl.
+  rewrite /envs_entails => ???? <-. rewrite envs_app_singleton_sound //=.
   rewrite -(from_affinely P') -(from_pure P) pure_True //.
   by rewrite affinely_True_emp affinely_emp emp_wand.
 Qed.
@@ -857,30 +886,30 @@ Qed.
 Lemma tac_pose_proof Δ Δ' j P Q :
   P →
   envs_app true (Esnoc Enil j P) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros HP ? <-. rewrite envs_app_singleton_sound //; simpl.
-  by rewrite -HP affinely_persistently_emp emp_wand.
+  rewrite /envs_entails => HP ? <-. rewrite envs_app_singleton_sound //=.
+  by rewrite -HP /= affinely_persistently_emp emp_wand.
 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.
+  envs_entails Δ'' Q → envs_entails Δ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
-  - rewrite envs_lookup_persistent_sound // envs_app_singleton_sound //; simpl.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
+  - rewrite envs_lookup_persistent_sound // envs_app_singleton_sound //=.
     by rewrite wand_elim_r.
-  - rewrite envs_lookup_sound // envs_app_singleton_sound //; simpl.
+  - rewrite envs_lookup_sound // envs_app_singleton_sound //=.
     by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_apply Δ Δ' i p R P1 P2 :
   envs_lookup_delete i Δ = Some (p, R, Δ') →
   IntoWand p false R P1 P2 →
-  (Δ' ⊢ P1) → Δ ⊢ P2.
+  envs_entails Δ' P1 → envs_entails Δ P2.
 Proof.
-  intros ?? HP1. rewrite envs_lookup_delete_sound //.
+  rewrite /envs_entails => ?? HP1. rewrite envs_lookup_delete_sound //.
   by rewrite into_wand /= HP1 wand_elim_l.
 Qed.
 
@@ -891,7 +920,7 @@ Lemma tac_rewrite Δ i p Pxy d Q :
     IntoInternalEq Pxy x y →
     (Q ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
-    (Δ ⊢ Φ (if d is Left then x else y)) → Δ ⊢ Q.
+    envs_entails Δ (Φ (if d is Left then x else y)) → envs_entails Δ Q.
 Proof.
   intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite'; auto.
   rewrite {1}envs_lookup_sound //.
@@ -907,30 +936,34 @@ Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
     (P ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
     envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ' →
-    (Δ' ⊢ Q) → Δ ⊢ Q.
+    envs_entails Δ' Q →
+    envs_entails Δ Q.
 Proof.
-  intros ?? A Δ' x y Φ HPxy HP ?? <-.
-  rewrite -(idemp bi_and Δ) {2}(envs_lookup_sound _ i) //.
-  rewrite (envs_simple_replace_singleton_sound _ _ j) //; simpl.
+  rewrite /envs_entails => ?? A Δ' x y Φ HPxy HP ?? <-.
+  rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
+  rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
   rewrite HP HPxy (affinely_persistently_if_elim _ (_ ≡ _)%I) sep_elim_l.
   rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
   rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
-  - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ Δ')%I). solve_proper.
+  - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
   - rewrite internal_eq_sym.
-    eapply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ Δ')%I). solve_proper.
+    eapply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
 Qed.
 
 (** * Conjunction splitting *)
 Lemma tac_and_split Δ P Q1 Q2 :
-  FromAnd P Q1 Q2 → (Δ ⊢ Q1) → (Δ ⊢ Q2) → Δ ⊢ P.
+  FromAnd P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ Q2 → envs_entails Δ P.
 Proof. intros. rewrite -(from_and P). by apply and_intro. Qed.
 
 (** * Separating conjunction splitting *)
 Lemma tac_sep_split Δ Δ1 Δ2 d js P Q1 Q2 :
   FromSep P Q1 Q2 →
   envs_split d js Δ = Some (Δ1,Δ2) →
-  (Δ1 ⊢ Q1) → (Δ2 ⊢ Q2) → Δ ⊢ P.
-Proof. intros ?? HQ1 HQ2. rewrite envs_split_sound //. by rewrite HQ1 HQ2. Qed.
+  envs_entails Δ1 Q1 → envs_entails Δ2 Q2 → envs_entails Δ P.
+Proof.
+  rewrite /envs_entails=>?? HQ1 HQ2.
+  rewrite envs_split_sound //. by rewrite HQ1 HQ2.
+Qed.
 
 (** * Combining *)
 Class FromSeps {PROP : bi} (P : PROP) (Qs : list PROP) :=
@@ -950,10 +983,10 @@ Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
   envs_lookup_delete_list js false Δ1 = Some (p, Ps, Δ2) →
   FromSeps P Ps →
   envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 →
-  (Δ3 ⊢ Q) → Δ1 ⊢ Q.
+  envs_entails Δ3 Q → envs_entails Δ1 Q.
 Proof.
-  intros ??? <-. rewrite envs_lookup_delete_list_sound //.
-  rewrite from_seps. rewrite envs_app_singleton_sound //; simpl.
+  rewrite /envs_entails => ??? <-. rewrite envs_lookup_delete_list_sound //.
+  rewrite from_seps. rewrite envs_app_singleton_sound //=.
   by rewrite wand_elim_r.
 Qed.
 
@@ -962,11 +995,11 @@ Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) →
   (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) →
   envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl. destruct p.
+  rewrite /envs_entails. intros. rewrite envs_simple_replace_sound //=. destruct p.
   - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
-  - by rewrite (into_sep P) right_id -(comm _ P1) wand_elim_r.
+  - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
 Qed.
 
 (* Using this tactic, one can destruct a (non-separating) conjunction in the
@@ -979,10 +1012,10 @@ Lemma tac_and_destruct_choice Δ Δ' i p d j P P1 P2 Q :
       (if d is Left then TCOr (Affine P2) (Absorbing Q)
        else TCOr (Affine P1) (Absorbing Q)))) →
   envs_simple_replace i p (Esnoc Enil j (if d is Left then P1 else P2)) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros ? HP ? HQ. rewrite envs_simple_replace_singleton_sound //; simpl.
-  destruct p.
+  rewrite /envs_entails => ? HP ? HQ.
+  rewrite envs_simple_replace_singleton_sound //=. destruct p.
   { rewrite (into_and _ P) HQ. destruct d; simpl.
     - by rewrite and_elim_l wand_elim_r.
     - by rewrite and_elim_r wand_elim_r. }
@@ -997,9 +1030,9 @@ Qed.
 
 (** * Framing *)
 Lemma tac_frame_pure Δ (φ : Prop) P Q :
-  φ → Frame true ⌜φ⌝ P Q → (Δ ⊢ Q) → Δ ⊢ P.
+  φ → Frame true ⌜φ⌝ P Q → envs_entails Δ Q → envs_entails Δ P.
 Proof.
-  intros ?? ->. rewrite -(frame ⌜φ⌝ P) /=.
+  rewrite /envs_entails => ?? ->. rewrite -(frame ⌜φ⌝ P) /=.
   rewrite -persistently_and_affinely_sep_l persistently_pure.
   auto using and_intro, pure_intro.
 Qed.
@@ -1007,26 +1040,32 @@ Qed.
 Lemma tac_frame Δ Δ' i p R P Q :
   envs_lookup_delete i Δ = Some (p, R, Δ') →
   Frame p R P Q →
-  ((if p then Δ else Δ') ⊢ Q) → Δ ⊢ P.
+  envs_entails (if p then Δ else Δ') Q → envs_entails Δ P.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
   - by rewrite envs_lookup_persistent_sound // -(frame R P) HQ.
   - rewrite envs_lookup_sound //; simpl. by rewrite -(frame R P) HQ.
 Qed.
 
 (** * Disjunction *)
-Lemma tac_or_l Δ P Q1 Q2 : FromOr P Q1 Q2 → (Δ ⊢ Q1) → Δ ⊢ P.
-Proof. intros. rewrite -(from_or P). by apply or_intro_l'. Qed.
-Lemma tac_or_r Δ P Q1 Q2 : FromOr P Q1 Q2 → (Δ ⊢ Q2) → Δ ⊢ P.
-Proof. intros. rewrite -(from_or P). by apply or_intro_r'. Qed.
+Lemma tac_or_l Δ P Q1 Q2 :
+  FromOr P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ P.
+Proof.
+  rewrite /envs_entails=> ? ->. rewrite -(from_or P). by apply or_intro_l'.
+Qed.
+Lemma tac_or_r Δ P Q1 Q2 :
+  FromOr P Q1 Q2 → envs_entails Δ Q2 → envs_entails Δ P.
+Proof.
+  rewrite /envs_entails=> ? ->. rewrite -(from_or P). by apply or_intro_r'.
+Qed.
 
 Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → IntoOr P P1 P2 →
   envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 →
   envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 →
-  (Δ1 ⊢ Q) → (Δ2 ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ1 Q → envs_entails Δ2 Q → envs_entails Δ Q.
 Proof.
-  intros ???? HP1 HP2. rewrite envs_lookup_sound //.
+  rewrite /envs_entails. intros ???? HP1 HP2. rewrite envs_lookup_sound //.
   rewrite (into_or P) affinely_persistently_if_or sep_or_r; apply or_elim.
   - rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
     by rewrite wand_elim_r.
@@ -1037,53 +1076,59 @@ Qed.
 (** * Forall *)
 Lemma tac_forall_intro {A} Δ (Φ : A → PROP) Q :
   FromForall Q Φ →
-  (∀ a, Δ ⊢ Φ a) →
-  Δ ⊢ Q.
-Proof. rewrite /FromForall=> <-. apply forall_intro. Qed.
+  (∀ a, envs_entails Δ (Φ a)) →
+  envs_entails Δ Q.
+Proof. rewrite /envs_entails /FromForall=> <-. apply forall_intro. Qed.
 
 Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → PROP) Q :
   envs_lookup i Δ = Some (p, P) → IntoForall P Φ →
   (∃ x : A,
     envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' ∧
-    (Δ' ⊢ Q)) →
-  Δ ⊢ Q.
+    envs_entails Δ' Q) →
+  envs_entails Δ Q.
 Proof.
-  intros ?? (x&?&?). rewrite envs_simple_replace_singleton_sound //; simpl.
+  rewrite /envs_entails. intros ?? (x&?&?).
+  rewrite envs_simple_replace_singleton_sound //; simpl.
   by rewrite (into_forall P) (forall_elim x) wand_elim_r.
 Qed.
 
 Lemma tac_forall_revert {A} Δ (Φ : A → PROP) :
-  (Δ ⊢ ∀ a, Φ a) → ∀ a, Δ ⊢ Φ a.
-Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.
+  envs_entails Δ (∀ a, Φ a) → ∀ a, envs_entails Δ (Φ a).
+Proof. rewrite /envs_entails => HΔ a. by rewrite HΔ (forall_elim a). Qed.
 
 (** * Existential *)
 Lemma tac_exist {A} Δ P (Φ : A → PROP) :
-  FromExist P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P.
-Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
+  FromExist P Φ → (∃ a, envs_entails Δ (Φ a)) → envs_entails Δ P.
+Proof.
+  rewrite /envs_entails => ? [a ?].
+  rewrite -(from_exist P). eauto using exist_intro'.
+Qed.
 
 Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → PROP) Q :
   envs_lookup i Δ = Some (p, P) → IntoExist P Φ →
   (∀ a, ∃ Δ',
-    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ' ∧ (Δ' ⊢ Q)) →
-  Δ ⊢ Q.
+    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ' ∧
+    envs_entails Δ' Q) →
+  envs_entails Δ Q.
 Proof.
-  intros ?? HΦ. rewrite envs_lookup_sound //.
+  rewrite /envs_entails => ?? HΦ. rewrite envs_lookup_sound //.
   rewrite (into_exist P) affinely_persistently_if_exist sep_exist_r.
   apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
   rewrite envs_simple_replace_singleton_sound' //; simpl. by rewrite wand_elim_r.
 Qed.
 
 (** * Modalities *)
-Lemma tac_modal_intro Δ P Q : FromModal P Q → (Δ ⊢ Q) → Δ ⊢ P.
-Proof. rewrite /FromModal. by intros <- ->. Qed.
+Lemma tac_modal_intro Δ P Q :
+  FromModal P Q → envs_entails Δ Q → envs_entails Δ P.
+Proof. by rewrite /envs_entails /FromModal=> <- ->. Qed.
 
 Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
   ElimModal P P' Q Q' →
   envs_replace i p false (Esnoc Enil i P') Δ = Some Δ' →
-  (Δ' ⊢ Q') → Δ ⊢ Q.
+  envs_entails Δ' Q' → envs_entails Δ Q.
 Proof.
-  intros ??? HΔ. rewrite envs_replace_singleton_sound //; simpl.
+  rewrite /envs_entails => ??? HΔ. rewrite envs_replace_singleton_sound //=.
   rewrite HΔ affinely_persistently_if_elim. by apply elim_modal.
 Qed.
 End bi_tactics.
@@ -1115,7 +1160,7 @@ Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
 Proof. by split. Qed.
 
 Lemma into_laterN_env_sound n Δ1 Δ2 :
-  IntoLaterNEnvs n Δ1 Δ2 → Δ1 ⊢ ▷^n (Δ2 : bi_car _).
+  IntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
 Proof.
   intros [Hp Hs]; rewrite /of_envs /= !laterN_and !laterN_sep.
   rewrite -{1}laterN_intro -laterN_affinely_persistently_2.
@@ -1128,15 +1173,20 @@ Proof.
 Qed.
 
 Lemma tac_next Δ Δ' n Q Q' :
-  FromLaterN n Q Q' → IntoLaterNEnvs n Δ Δ' → (Δ' ⊢ Q') → Δ ⊢ Q.
-Proof. intros ?? HQ. by rewrite -(from_laterN n Q) into_laterN_env_sound HQ. Qed.
+  FromLaterN n Q Q' → IntoLaterNEnvs n Δ Δ' →
+  envs_entails Δ' Q' → envs_entails Δ Q.
+Proof.
+  rewrite /envs_entails => ?? HQ.
+    by rewrite -(from_laterN n Q) into_laterN_env_sound HQ.
+Qed.
 
 Lemma tac_löb Δ Δ' i Q :
   env_spatial_is_nil Δ = true →
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros ?? HQ. rewrite (env_spatial_is_nil_affinely_persistently Δ) //.
+  rewrite /envs_entails => ?? HQ.
+  rewrite (env_spatial_is_nil_affinely_persistently Δ) //.
   rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
   rewrite -(löb (bi_persistently Q)%I) later_persistently. apply impl_intro_l.
   rewrite envs_app_singleton_sound //; simpl; rewrite HQ.
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 7e6798cbc1ec5c09739cfc8e933503eee19bee33..9ee7c2e7fefc17516a29c8ebc5f7af5a0547e1bd 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -11,18 +11,19 @@ Notation "" := Enil (only printing) : proof_scope.
 Notation "Γ H : P" := (Esnoc Γ H P)
   (at level 1, P at level 200,
    left associativity, format "Γ H  :  P '//'", only printing) : proof_scope.
+
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
-  (of_envs (Envs Γ Δ) ⊢ Q%I)
+  (envs_entails (Envs Γ Δ) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
   C_scope.
 Notation "Δ '--------------------------------------' ∗ Q" :=
-  (of_envs (Envs Enil Δ) ⊢ Q%I)
+  (envs_entails (Envs Enil Δ) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
 Notation "Γ '--------------------------------------' □ Q" :=
-  (of_envs (Envs Γ Enil) ⊢ Q%I)
+  (envs_entails (Envs Γ Enil) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Γ '--------------------------------------' □ '//' Q '//'", only printing)  : C_scope.
-Notation "'--------------------------------------' ∗ Q" := (of_envs (Envs Enil Enil) ⊢ Q%I)
+Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil) Q%I)
   (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index e27d3b1950e7205711ff2ba91b3df11eec19ddbb..77086288bc914a107f18d6fd76a5c41037f17ebd 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
-From iris.bi Require Export bi.
+From iris.bi Require Export bi big_op.
 From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
 From stdpp Require Import stringmap hlist.
@@ -22,7 +22,7 @@ Ltac env_reflexivity := env_cbv; exact eq_refl.
 (* Tactic Notation tactics cannot return terms *)
 Ltac iFresh' H :=
   lazymatch goal with
-  |- of_envs ?Δ ⊢ _ =>
+  |- envs_entails ?Δ _ =>
      (* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
      first use [cbv] to compute the domain of [Δ] *)
      let Hs := eval cbv in (envs_dom Δ) in
@@ -34,14 +34,14 @@ Ltac iFresh := iFresh' "~".
 Ltac iMissingHyps Hs :=
   let Δ :=
     lazymatch goal with
-    | |- of_envs ?Δ ⊢ _ => Δ
+    | |- envs_entails ?Δ _ => Δ
     | |- context[ envs_split _ _ ?Δ ] => Δ
     end in
   let Hhyps := eval env_cbv in (envs_dom Δ) in
   eval vm_compute in (list_difference Hs Hhyps).
 
 Ltac iTypeOf H :=
-  let Δ := match goal with |- of_envs ?Δ ⊢ _ => Δ end in
+  let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
   eval env_cbv in (envs_lookup H Δ).
 
 Tactic Notation "iMatchHyp" tactic1(tac) :=
@@ -64,7 +64,7 @@ Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
 (** * Start a proof *)
 Ltac iStartProof :=
   lazymatch goal with
-  | |- of_envs _ ⊢ _ => idtac
+  | |- envs_entails _ _ => idtac
   | |- let _ := _ in _ => fail
   | |- ?P =>
     apply (proj2 (_ : AsValid P _)), tac_adequate
@@ -101,7 +101,7 @@ Ltac iElaborateSelPat pat :=
        end
     end in
   lazymatch goal with
-  | |- of_envs ?Δ ⊢ _ =>
+  | |- envs_entails ?Δ _ =>
     let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
   end.
 
@@ -167,7 +167,7 @@ Tactic Notation "iAssumption" :=
        |find p Γ Q]
     end in
   lazymatch goal with
-  | |- of_envs (Envs ?Γp ?Γs) ⊢ ?Q =>
+  | |- envs_entails (Envs ?Γp ?Γs) ?Q =>
      first [find true Γp Q | find false Γs Q
            |fail "iAssumption:" Q "not found"]
   end.
@@ -216,8 +216,8 @@ Tactic Notation "iPureIntro" :=
 Local Ltac iFrameFinish :=
   lazy iota beta;
   try match goal with
-  | |- _ ⊢ True => exact (bi.pure_intro _ _ I)
-  | |- _ ⊢ emp => iEmpIntro
+  | |- envs_entails _ True => exact (bi.pure_intro _ _ I)
+  | |- envs_entails _ emp => iEmpIntro
   end.
 
 Local Ltac iFramePure t :=
@@ -241,7 +241,7 @@ Local Ltac iFrameAnyPersistent :=
   let rec go Hs :=
     match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
   match goal with
-  | |- of_envs ?Δ ⊢ _ =>
+  | |- envs_entails ?Δ _ =>
      let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
   end.
 
@@ -249,7 +249,7 @@ Local Ltac iFrameAnySpatial :=
   let rec go Hs :=
     match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
   match goal with
-  | |- of_envs ?Δ ⊢ _ =>
+  | |- envs_entails ?Δ _ =>
      let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
   end.
 
@@ -312,7 +312,7 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
 Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
   try iStartProof;
   lazymatch goal with
-  | |- _ ⊢ _ =>
+  | |- envs_entails _ _ =>
     eapply tac_forall_intro;
       [apply _ ||
        let P := match goal with |- FromForall ?P _ => P end in
@@ -379,14 +379,14 @@ Local Tactic Notation "iIntroForall" :=
   lazymatch goal with
   | |- ∀ _, ?P => fail (* actually an →, this is handled by iIntro below *)
   | |- ∀ _, _ => intro
-  | |- _ ⊢ (∀ x : _, _) => let x' := fresh x in iIntro (x')
+  | |- envs_entails _ (∀ x : _, _) => let x' := fresh x in iIntro (x')
   end.
 Local Tactic Notation "iIntro" :=
   try iStartProof;
   lazymatch goal with
   | |- _ → ?P => intro
-  | |- _ ⊢ (_ -∗ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
-  | |- _ ⊢ (_ → _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+  | |- envs_entails _ (_ -∗ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+  | |- envs_entails _ (_ → _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
   end.
 
 (** * Specialize *)
@@ -736,13 +736,10 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
 (** * Conjunction and separating conjunction *)
 Tactic Notation "iSplit" :=
   iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ _ =>
-    eapply tac_and_split;
-      [apply _ ||
-       let P := match goal with |- FromAnd ?P _ _ => P end in
-       fail "iSplit:" P "not a conjunction"| |]
-  end.
+  eapply tac_and_split;
+    [apply _ ||
+     let P := match goal with |- FromAnd ?P _ _ => P end in
+     fail "iSplit:" P "not a conjunction"| |].
 
 Tactic Notation "iSplitL" constr(Hs) :=
   iStartProof;
@@ -859,7 +856,7 @@ Tactic Notation "iAlways":=
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
   iStartProof;
-  let P := match goal with |- _ ⊢ ?P => P end in
+  let P := match goal with |- envs_entails _ ?P => P end in
   try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end;
   eapply (tac_next _ _ n);
     [apply _ || fail "iNext:" P "does not contain" n "laters"
@@ -1410,7 +1407,7 @@ result in the following actions:
 Tactic Notation "iInductionCore" constr(x) "as" simple_intropattern(pat) constr(IH) :=
   let rec fix_ihs :=
     lazymatch goal with
-    | H : context [coq_tactics.of_envs _ ⊢ _] |- _ =>
+    | H : context [envs_entails _ _] |- _ =>
        eapply (tac_revert_ih _ _ _ H _);
          [reflexivity
           || fail "iInduction: spatial context not empty, this should not happen"|];
@@ -1430,8 +1427,8 @@ Ltac iHypsContaining x :=
        | _ => go Γ x Hs
        end
      end in
-  let Γp := lazymatch goal with |- of_envs (Envs ?Γp _) ⊢ _ => Γp end in
-  let Γs := lazymatch goal with |- of_envs (Envs _ ?Γs) ⊢ _ => Γs end in
+  let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _) _ => Γp end in
+  let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs) _ => Γs end in
   let Hs := go Γp x (@nil string) in go Γs x Hs.
 
 Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic(tac) :=
@@ -1759,25 +1756,34 @@ Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
 Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
   iDestructCore lem as false (fun H => iModCore H; iPure H as pat).
 
+Hint Extern 0 (_ ⊢ _) => iStartProof.
+
 (* Make sure that by and done solve trivial things in proof mode *)
-Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
-Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
-Hint Extern 0 (of_envs _ ⊢ emp) => iEmpIntro.
-Hint Resolve bi.internal_eq_refl. (* Maybe make an [iReflexivity] tactic *)
-
-(* For iIntros we do not check whether we are in proof mode because we actually
-want it to enter proof mode when we are not already in it. *)
-Hint Extern 0 (_ ⊢ _) => progress iIntros.
-
-Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
-Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
-Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
-Hint Extern 1 (of_envs _ ⊢ bi_plainly _) => iAlways.
-Hint Extern 1 (of_envs _ ⊢ bi_persistently _) => iAlways.
-Hint Extern 1 (of_envs _ ⊢ bi_affinely _) => iAlways.
-Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
-Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.
-Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iLeft.
-Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iRight.
-
-Hint Extern 2 (of_envs _ ⊢ _ ∗ _) => progress iFrame : iFrame.
+Hint Extern 0 (envs_entails _ _) => iPureIntro; try done.
+Hint Extern 0 (envs_entails _ _) => iAssumption.
+Hint Extern 0 (envs_entails _ emp) => iEmpIntro.
+
+(* TODO: look for a more principled way of adding trivial hints like those
+below; see the discussion in !75 for further details. *)
+Hint Extern 0 (envs_entails _ (_ ≡ _)) => apply bi.internal_eq_refl.
+Hint Extern 0 (envs_entails _ (big_opL _ _ _)) => apply bi.big_sepL_nil'.
+Hint Extern 0 (envs_entails _ (big_opM _ _ _)) => apply bi.big_sepM_empty'.
+Hint Extern 0 (envs_entails _ (big_opS _ _ _)) => apply bi.big_sepS_empty'.
+Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) => apply bi.big_sepMS_empty'.
+
+Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros.
+Hint Extern 0 (envs_entails _ (_ → _)) => iIntros.
+Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros.
+
+Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit.
+Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit.
+Hint Extern 1 (envs_entails _ (â–· _)) => iNext.
+Hint Extern 1 (envs_entails _ (bi_plainly _)) => iAlways.
+Hint Extern 1 (envs_entails _ (bi_persistently _)) => iAlways.
+Hint Extern 1 (envs_entails _ (bi_affinely _)) => iAlways.
+Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _.
+Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro.
+Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft.
+Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight.
+
+Hint Extern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 5fedc7f4cd2cf9a618b7c9d938dcbdbcd2920b3f..6834c5c5e3928fd626f706c6eda0a8daf90d433e 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -101,7 +101,7 @@ update modalities (which we did not cover in the paper). Normally we use these
 mask changing update modalities directly in our proofs, but in this file we use
 the first prove the rule as a lemma, and then use that. *)
 Lemma wp_inv_open `{irisG Λ Σ} N E P e Φ :
-  nclose N ⊆ E → atomic e →
+  nclose N ⊆ E → Atomic e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".
diff --git a/theories/tests/one_shot.v b/theories/tests/one_shot.v
index 2097a1b672286109cdd505760453b8ce94cc8fe2..566f525801ab8e67eacf332228bbd2fb34ca33e2 100644
--- a/theories/tests/one_shot.v
+++ b/theories/tests/one_shot.v
@@ -21,8 +21,8 @@ Definition one_shot_example : val := λ: <>,
     end)).
 
 Definition one_shotR := csumR (exclR unitC) (agreeR ZC).
-Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
-Definition Shot (n : Z) : one_shotR := (Cinr (to_agree n) : one_shotR).
+Definition Pending : one_shotR := Cinl (Excl ()).
+Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
 
 Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
 Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index b97d642d2bd159e41380556e34ce572d9f2078b0..38ac3dbdf83b535334225309b6027786c2bb608e 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -62,6 +62,9 @@ Proof. iIntros "H1 #H2". by iFrame. Qed.
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
 Proof. iIntros (??) "H". auto. Qed.
 
+Lemma test_iIntros_pure_not : (⌜ ¬False ⌝ : PROP)%I.
+Proof. by iIntros (?). Qed.
+
 Lemma test_fast_iIntros P Q :
   (∀ x y z : nat,
     ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x))%I.
@@ -137,7 +140,7 @@ Qed.
 
 Lemma test_eauto_iFrame P Q R `{!Persistent R} :
   P -∗ Q -∗ R → R ∗ Q ∗ P ∗ R ∨ False.
-Proof. eauto with iFrame. Qed.
+Proof. eauto 10 with iFrame. Qed.
 
 Lemma test_iCombine_persistent P Q R `{!Persistent R} :
   P -∗ Q -∗ R → R ∗ Q ∗ P ∗ R ∨ False.
@@ -247,11 +250,4 @@ Lemma test_iAlways P Q R :
   □ P -∗ bi_persistently Q → R -∗ bi_persistently (bi_affinely (bi_affinely P)) ∗ □ Q.
 Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
 
-(* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
-8.6 support. See also issue #108. *)
-(*
-Lemma test_iIntros_pure : (⌜ ¬False ⌝ : uPred M)%I.
-Proof. by iIntros (?). Qed.
-*)
-
 End tests.