diff --git a/algebra/agree.v b/algebra/agree.v
index a71d7a4d218576cbf7067f507fc73d52badf2e3f..58a8e6b6b362c3a7433371b1e63e14cf1a3aa07f 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -132,9 +132,9 @@ Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
 
 (** Internalized properties *)
 Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b)%I ≡ (a ≡ b : uPred M)%I.
-Proof. split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne. Qed.
+Proof. do 2 split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne. Qed.
 Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊑ (x ≡ y : uPred M).
-Proof. by intros r n _ ?; apply: agree_op_inv. Qed.
+Proof. split=> r n _ ?; by apply: agree_op_inv. Qed.
 End agree.
 
 Arguments agreeC : clear implicits.
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 5931c648af4dcf01f7311413df68562460c2829c..57474621fedceff8d665a0f3db3ad5ead79e701d 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -60,8 +60,8 @@ Proof.
 Qed.
 
 Lemma dec_agree_equivI {M} a b : (DecAgree a ≡ DecAgree b)%I ≡ (a = b : uPred M)%I.
-Proof. split. by case. by destruct 1. Qed.
+Proof. do 2 split. by case. by destruct 1. Qed.
 Lemma dec_agree_validI {M} (x y : dec_agreeRA) : ✓ (x ⋅ y) ⊑ (x = y : uPred M).
-Proof. intros r n _ ?. by apply: dec_agree_op_inv. Qed.
+Proof. split=> r n _ ?. by apply: dec_agree_op_inv. Qed.
 
 End dec_agree.
diff --git a/algebra/excl.v b/algebra/excl.v
index 58298171440115c97b2385a3dc9d0e7f78684394..656bcae8e3bd1d3f2ca903de33861b3c0addad83 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -145,7 +145,7 @@ Lemma excl_equivI {M} (x y : excl A) :
                | ExclUnit, ExclUnit | ExclBot, ExclBot => True
                | _, _ => False
                end : uPred M)%I.
-Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
+Proof. do 2 split. by destruct 1. by destruct x, y; try constructor. Qed.
 Lemma excl_validI {M} (x : excl A) :
   (✓ x)%I ≡ (if x is ExclBot then False else True : uPred M)%I.
 Proof. by destruct x. Qed.
diff --git a/algebra/option.v b/algebra/option.v
index 7ae362ec1683bbf0997c2f1d4594cc59fa16f33f..7a020107ec4a97ddc17bf63c831392e3c9dfdd2a 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -138,7 +138,7 @@ Lemma option_equivI {M} (x y : option A) :
   (x ≡ y)%I ≡ (match x, y with
                | Some a, Some b => a ≡ b | None, None => True | _, _ => False
                end : uPred M)%I.
-Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
+Proof. do 2 split. by destruct 1. by destruct x, y; try constructor. Qed.
 Lemma option_validI {M} (x : option A) :
   (✓ x)%I ≡ (match x with Some a => ✓ a | None => True end : uPred M)%I.
 Proof. by destruct x. Qed.
diff --git a/algebra/upred.v b/algebra/upred.v
index 0e1f6ea1d1aa15f6b113db6cc11744f91f31f8e9..e3b92d621f55f2586d2aaf9752276954293d02ed 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -21,10 +21,13 @@ Arguments uPred_holds {_} _%I _ _.
 
 Section cofe.
   Context {M : cmraT}.
-  Instance uPred_equiv : Equiv (uPred M) := λ P Q, ∀ n x,
-    ✓{n} x → P n x ↔ Q n x.
-  Instance uPred_dist : Dist (uPred M) := λ n P Q, ∀ n' x,
-    n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x.
+
+  Inductive uPred_equiv' (P Q : uPred M) : Prop :=
+    { uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
+  Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
+  Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
+    { uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x }.
+  Instance uPred_dist : Dist (uPred M) := uPred_dist'.
   Program Instance uPred_compl : Compl (uPred M) := λ c,
     {| uPred_holds n x := c (S n) n x |}.
   Next Obligation. by intros c n x y ??; simpl in *; apply uPred_ne with x. Qed.
@@ -35,14 +38,16 @@ Section cofe.
   Definition uPred_cofe_mixin : CofeMixin (uPred M).
   Proof.
     split.
-    - intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
-      intros HPQ n x ?; apply HPQ with n; auto.
+    - intros P Q; split.
+      + by intros HPQ n; split=> i x ??; apply HPQ.
+      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
     - intros n; split.
-      + by intros P x i.
-      + by intros P Q HPQ x i ??; symmetry; apply HPQ.
-      + by intros P Q Q' HP HQ i x ??; trans (Q i x);[apply HP|apply HQ].
-    - intros n P Q HPQ i x ??; apply HPQ; auto.
-    - intros n c i x ??; symmetry; apply (chain_cauchy c i (S n)); auto.
+      + by intros P; split=> x i.
+      + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
+      + intros P Q Q' HP HQ; split=> i x ??.
+        by trans (Q i x);[apply HP|apply HQ].
+    - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
+    - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i (S n)); auto.
   Qed.
   Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
 End cofe.
@@ -71,30 +76,32 @@ Qed.
 Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
   `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
 Proof.
-  by intros x1 x2 Hx n' y; split; apply Hx; auto using validN_preserving.
+  intros x1 x2 Hx; split=> n' y ??.
+  split; apply Hx; auto using validN_preserving.
 Qed.
 Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P ≡ P.
-Proof. by intros n x ?. Qed.
+Proof. by split=> n x ?. Qed.
 Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
     `{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
   uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
-Proof. by intros n x Hx. Qed.
+Proof. by split=> n x Hx. Qed.
 Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
-    `{!CMRAMonotone f, !CMRAMonotone g} :
-  (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
-Proof. move=> Hfg x P n Hx /=. by rewrite /uPred_holds /= Hfg. Qed.
+      `{!CMRAMonotone f} `{!CMRAMonotone g}:
+  (∀ x, f x ≡ g x) -> ∀ x, uPred_map f x ≡ uPred_map g x.
+Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
 Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
   uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
 Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
     `{!CMRAMonotone f, !CMRAMonotone g} n :
   f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
 Proof.
-  by intros Hfg P n' y ??;
+  by intros Hfg P; split=> n' y ??;
     rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
 Qed.
 
 (** logical entailement *)
-Definition uPred_entails {M} (P Q : uPred M) := ∀ n x, ✓{n} x → P n x → Q n x.
+Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
+  { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
 Hint Extern 0 (uPred_entails _ _) => reflexivity.
 Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
 
@@ -218,9 +225,9 @@ Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%
 Infix "↔" := uPred_iff : uPred_scope.
 
 Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊑ (P ∨ ▷ False).
-Arguments timelessP {_} _ {_} _ _ _ _.
+Arguments timelessP {_} _ {_}.
 Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P.
-Arguments always_stable {_} _ {_} _ _ _ _.
+Arguments always_stable {_} _ {_}.
 
 Module uPred. Section uPred_logic.
 Context {M : cmraT}.
@@ -229,15 +236,20 @@ Implicit Types P Q : uPred M.
 Implicit Types A : Type.
 Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
 Arguments uPred_holds {_} !_ _ _ /.
+Hint Immediate uPred_in_entails.
 
 Global Instance: PreOrder (@uPred_entails M).
-Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
+Proof.
+  split.
+  * by intros P; split=> x i.
+  * by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
+Qed.
 Global Instance: AntiSymm (≡) (@uPred_entails M).
-Proof. intros P Q HPQ HQP; split; auto. Qed.
+Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
 Lemma equiv_spec P Q : P ≡ Q ↔ P ⊑ Q ∧ Q ⊑ P.
 Proof.
   split; [|by intros [??]; apply (anti_symm (⊑))].
-  intros HPQ; split; intros x i; apply HPQ.
+  intros HPQ; split; split=> x i; apply HPQ.
 Qed.
 Lemma equiv_entails P Q : P ≡ Q → P ⊑ Q.
 Proof. apply equiv_spec. Qed.
@@ -253,31 +265,34 @@ Qed.
 
 (** Non-expansiveness and setoid morphisms *)
 Global Instance const_proper : Proper (iff ==> (≡)) (@uPred_const M).
-Proof. by intros φ1 φ2 Hφ [|n] ??; try apply Hφ. Qed.
+Proof. intros φ1 φ2 Hφ. by split=> -[|n] ?; try apply Hφ. Qed.
 Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
 Proof.
-  intros P P' HP Q Q' HQ; split; intros [??]; split; by apply HP || by apply HQ.
+  intros P P' HP Q Q' HQ; split=> x n' ??.
+  split; (intros [??]; split; [by apply HP|by apply HQ]).
 Qed.
 Global Instance and_proper :
   Proper ((≡) ==> (≡) ==> (≡)) (@uPred_and M) := ne_proper_2 _.
 Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
 Proof.
-  intros P P' HP Q Q' HQ; split; intros [?|?];
-    first [by left; apply HP | by right; apply HQ].
+  intros P P' HP Q Q' HQ; split=> x n' ??.
+  split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
 Qed.
 Global Instance or_proper :
   Proper ((≡) ==> (≡) ==> (≡)) (@uPred_or M) := ne_proper_2 _.
 Global Instance impl_ne n :
   Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
 Proof.
-  intros P P' HP Q Q' HQ; split; intros HPQ x' n'' ????; apply HQ,HPQ,HP; auto.
+  intros P P' HP Q Q' HQ; split=> x n' ??.
+  split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
 Qed.
 Global Instance impl_proper :
   Proper ((≡) ==> (≡) ==> (≡)) (@uPred_impl M) := ne_proper_2 _.
 Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
 Proof.
-  intros P P' HP Q Q' HQ n' x ??; split; intros (x1&x2&?&?&?); cofe_subst x;
-    exists x1, x2; split_and?; try (apply HP || apply HQ);
+  intros P P' HP Q Q' HQ; split=> n' x ??.
+  split; intros (x1&x2&?&?&?); cofe_subst x;
+    exists x1, x2; split_and!; try (apply HP || apply HQ);
     eauto using cmra_validN_op_l, cmra_validN_op_r.
 Qed.
 Global Instance sep_proper :
@@ -285,7 +300,7 @@ Global Instance sep_proper :
 Global Instance wand_ne n :
   Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
 Proof.
-  intros P P' HP Q Q' HQ n' x ??; split; intros HPQ n'' x' ???;
+  intros P P' HP Q Q' HQ; split=> n' x ??; split; intros HPQ x' n'' ???;
     apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
 Qed.
 Global Instance wand_proper :
@@ -293,41 +308,51 @@ Global Instance wand_proper :
 Global Instance eq_ne (A : cofeT) n :
   Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
 Proof.
-  intros x x' Hx y y' Hy n' z; split; intros; simpl in *.
-  - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
-  - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
+  intros x x' Hx y y' Hy; split=> n' z; split; intros; simpl in *.
+  * by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
+  * by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
 Qed.
 Global Instance eq_proper (A : cofeT) :
   Proper ((≡) ==> (≡) ==> (≡)) (@uPred_eq M A) := ne_proper_2 _.
-Global Instance forall_ne A :
+Global Instance forall_ne A n :
   Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
-Proof. by intros n Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed.
+Proof. by intros Ψ1 Ψ2 HΨ; split=> n' x; split; intros HP a; apply HΨ. Qed.
 Global Instance forall_proper A :
   Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_forall M A).
-Proof. by intros Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed.
-Global Instance exist_ne A :
+Proof. by intros Ψ1 Ψ2 HΨ; split=> n' x; split; intros HP a; apply HΨ. Qed.
+Global Instance exist_ne A n :
   Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
-Proof. by intros n P1 P2 HP x; split; intros [a ?]; exists a; apply HP. Qed.
+Proof.
+  intros Ψ1 Ψ2 HΨ; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
+Qed.
 Global Instance exist_proper A :
   Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_exist M A).
-Proof. by intros P1 P2 HP n' x; split; intros [a ?]; exists a; apply HP. Qed.
+Proof.
+  intros Ψ1 Ψ2 HΨ; split=> n' x ?; split; intros [a ?]; exists a; by apply HΨ.
+Qed.
 Global Instance later_contractive : Contractive (@uPred_later M).
 Proof.
-  intros n P Q HPQ [|n'] x ??; simpl; [done|].
+  intros n P Q HPQ; split=> -[|n'] x ??; simpl; [done|].
   apply (HPQ n'); eauto using cmra_validN_S.
 Qed.
 Global Instance later_proper :
   Proper ((≡) ==> (≡)) (@uPred_later M) := ne_proper _.
-Global Instance always_ne n: Proper (dist n ==> dist n) (@uPred_always M).
-Proof. intros P1 P2 HP n' x; split; apply HP; eauto using cmra_unit_validN. Qed.
+Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
+Proof.
+  intros P1 P2 HP; split=> n' x; split; apply HP; eauto using cmra_unit_validN.
+Qed.
 Global Instance always_proper :
   Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _.
 Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
-Proof. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed.
+Proof.
+  intros a b Ha; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
+Qed.
 Global Instance ownM_proper: Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _.
 Global Instance valid_ne {A : cmraT} n :
-  Proper (dist n ==> dist n) (@uPred_valid M A).
-Proof. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed.
+Proper (dist n ==> dist n) (@uPred_valid M A).
+Proof.
+  intros a b Ha; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
+Qed.
 Global Instance valid_proper {A : cmraT} :
   Proper ((≡) ==> (≡)) (@uPred_valid M A) := ne_proper _.
 Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
@@ -337,43 +362,45 @@ Global Instance iff_proper :
 
 (** Introduction and elimination rules *)
 Lemma const_intro φ P : φ → P ⊑ ■ φ.
-Proof. by intros ???. Qed.
+Proof. by intros ?; split. Qed.
 Lemma const_elim φ Q R : Q ⊑ ■ φ → (φ → Q ⊑ R) → Q ⊑ R.
-Proof. intros HQP HQR n x ??; apply HQR; first eapply (HQP n); eauto. Qed.
+Proof. intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto. Qed.
 Lemma False_elim P : False ⊑ P.
-Proof. by intros n x ?. Qed.
+Proof. by split=> n x ?. Qed.
 Lemma and_elim_l P Q : (P ∧ Q) ⊑ P.
-Proof. by intros n x ? [??]. Qed.
+Proof. by split=> n x ? [??]. Qed.
 Lemma and_elim_r P Q : (P ∧ Q) ⊑ Q.
-Proof. by intros n x ? [??]. Qed.
+Proof. by split=> n x ? [??]. Qed.
 Lemma and_intro P Q R : P ⊑ Q → P ⊑ R → P ⊑ (Q ∧ R).
-Proof. intros HQ HR n x ??; split; auto. Qed.
+Proof. intros HQ HR; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
 Lemma or_intro_l P Q : P ⊑ (P ∨ Q).
-Proof. intros n x ??; left; auto. Qed.
+Proof. split=> n x ??; left; auto. Qed.
 Lemma or_intro_r P Q : Q ⊑ (P ∨ Q).
-Proof. intros n x ??; right; auto. Qed.
+Proof. split=> n x ??; right; auto. Qed.
 Lemma or_elim P Q R : P ⊑ R → Q ⊑ R → (P ∨ Q) ⊑ R.
-Proof. intros HP HQ n x ? [?|?]. by apply HP. by apply HQ. Qed.
+Proof. intros HP HQ; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
 Lemma impl_intro_r P Q R : (P ∧ Q) ⊑ R → P ⊑ (Q → R).
 Proof.
-  intros HQ; repeat intro; apply HQ; naive_solver eauto using uPred_weaken.
+  intros HQ; split=> n x ?? n' x' ????.
+  apply HQ; naive_solver eauto using uPred_weaken.
 Qed.
 Lemma impl_elim P Q R : P ⊑ (Q → R) → P ⊑ Q → P ⊑ R.
-Proof. by intros HP HP' n x ??; apply HP with n x, HP'. Qed.
+Proof. by intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
 Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊑ Ψ a) → P ⊑ (∀ a, Ψ a).
-Proof. by intros HPΨ n x ?? a; apply HPΨ. Qed.
+Proof. by intros HPΨ; split=> n x ?? a; apply HPΨ. Qed.
 Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊑ Ψ a.
-Proof. intros n x ? HP; apply HP. Qed.
+Proof. split=> n x ? HP; apply HP. Qed.
 Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊑ (∃ a, Ψ a).
-Proof. by intros n x ??; exists a. Qed.
+Proof. by split=> n x ??; exists a. Qed.
 Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊑ Q) → (∃ a, Φ a) ⊑ Q.
-Proof. by intros HΦΨ n x ? [a ?]; apply HΦΨ with a. Qed.
+Proof. by intros HΦΨ; split=> n x ? [a ?]; apply HΦΨ with a. Qed.
 Lemma eq_refl {A : cofeT} (a : A) P : P ⊑ (a ≡ a).
-Proof. by intros n x ??; simpl. Qed.
+Proof. by split=> n x ??; simpl. Qed.
 Lemma eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P
   `{HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : P ⊑ (a ≡ b) → P ⊑ Ψ a → P ⊑ Ψ b.
 Proof.
-  intros Hab Ha n x ??; apply HΨ with n a; auto. by symmetry; apply Hab with x.
+  intros Hab Ha; split=> n x ??.
+  apply HΨ with n a; auto. by symmetry; apply Hab with x. by apply Ha.
 Qed.
 Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
   True ⊑ (a ≡ b) → a ≡ b.
@@ -382,7 +409,7 @@ Proof.
   apply cmra_valid_validN, cmra_empty_valid.
 Qed.
 Lemma iff_equiv P Q : True ⊑ (P ↔ Q) → P ≡ Q.
-Proof. by intros HPQ n x ?; split; intros; apply HPQ with n x. Qed.
+Proof. by intros HPQ; split=> n x ?; split; intros; apply HPQ with n x. Qed.
 
 (* Derived logical stuff *)
 Lemma True_intro P : P ⊑ True.
@@ -552,23 +579,23 @@ Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto using eq_refl. solve_ne. Q
 (* BI connectives *)
 Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
 Proof.
-  intros HQ HQ' n' x ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
-    eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
+  intros HQ HQ'; split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x;
+    eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
 Qed.
 Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
 Proof.
-  intros P n x Hvalid; split.
+  intros P; split=> n x Hvalid; split.
   - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
   - by intros ?; exists (unit x), x; rewrite cmra_unit_l.
 Qed. 
 Global Instance sep_comm : Comm (≡) (@uPred_sep M).
 Proof.
-  by intros P Q n x ?; split;
+  by intros P Q; split=> n x ?; split;
     intros (x1&x2&?&?&?); exists x2, x1; rewrite (comm op).
 Qed.
 Global Instance sep_assoc : Assoc (≡) (@uPred_sep M).
 Proof.
-  intros P Q R n x ?; split.
+  intros P Q R; split=> n x ?; split.
   - intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 â‹… y1), y2; split_and?; auto.
     + by rewrite -(assoc op) -Hy -Hx.
     + by exists x1, y1.
@@ -578,12 +605,12 @@ Proof.
 Qed.
 Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
 Proof.
-  intros HPQR n x ?? n' x' ???; apply HPQR; auto.
+  intros HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
   exists x, x'; split_and?; auto.
   eapply uPred_weaken with n x; eauto using cmra_validN_op_l.
 Qed.
 Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q.
-Proof. by intros n x ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
+Proof. by split; intros n x ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
 
 (* Derived BI Stuff *)
 Hint Resolve sep_mono.
@@ -688,10 +715,10 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 Lemma always_const φ : (□ ■ φ : uPred M)%I ≡ (■ φ)%I.
 Proof. done. Qed.
 Lemma always_elim P : □ P ⊑ P.
-Proof. intros n x ?; simpl; eauto using uPred_weaken, cmra_included_unit. Qed.
+Proof. split=> n x ?; simpl; eauto using uPred_weaken, cmra_included_unit. Qed.
 Lemma always_intro' P Q : □ P ⊑ Q → □ P ⊑ □ Q.
 Proof.
-  intros HPQ n x ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
+  intros HPQ; split=> n x ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
   by rewrite cmra_unit_idemp.
 Qed.
 Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
@@ -704,11 +731,11 @@ Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a)%I ≡ (∃ a, 
 Proof. done. Qed.
 Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊑ □ (P ★ Q).
 Proof.
-  intros n x ? [??]; exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
+  split=> n x ? [??]; exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
 Qed.
 Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊑ (□ P ★ Q).
 Proof.
-  intros n x ? [??]; exists (unit x), x; simpl in *.
+  split=> n x ? [??]; exists (unit x), x; simpl in *.
   by rewrite cmra_unit_l cmra_unit_idemp.
 Qed.
 Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
@@ -720,6 +747,9 @@ Proof. intros. apply always_intro'. by rewrite always_elim. Qed.
 Hint Resolve always_mono.
 Global Instance always_mono' : Proper ((⊑) ==> (⊑)) (@uPred_always M).
 Proof. intros P Q; apply always_mono. Qed.
+Global Instance always_flip_mono' :
+  Proper (flip (⊑) ==> flip (⊑)) (@uPred_always M).
+Proof. intros P Q; apply always_mono. Qed.
 Lemma always_impl P Q : □ (P → Q) ⊑ (□ P → □ Q).
 Proof.
   apply impl_intro_l; rewrite -always_and.
@@ -730,7 +760,7 @@ Proof.
   apply (anti_symm (⊑)); auto using always_elim.
   apply (eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
   { intros n; solve_proper. }
-  rewrite -(eq_refl _ True) always_const; auto.
+  rewrite -(eq_refl a True) always_const; auto.
 Qed.
 Lemma always_and_sep P Q : (□ (P ∧ Q))%I ≡ (□ (P ★ Q))%I.
 Proof. apply (anti_symm (⊑)); auto using always_and_sep_1. Qed.
@@ -757,33 +787,35 @@ Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
 
 (* Later *)
 Lemma later_mono P Q : P ⊑ Q → ▷ P ⊑ ▷ Q.
-Proof. intros HP [|n] x ??; [done|apply HP; eauto using cmra_validN_S]. Qed.
+Proof.
+  intros HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
+Qed.
 Lemma later_intro P : P ⊑ ▷ P.
 Proof.
-  intros [|n] x ??; simpl in *; [done|].
+  split=> -[|n] x ??; simpl in *; [done|].
   apply uPred_weaken with (S n) x; eauto using cmra_validN_S.
 Qed.
 Lemma löb P : (▷ P → P) ⊑ P.
 Proof.
-  intros n x ? HP; induction n as [|n IH]; [by apply HP|].
+  split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
   apply HP, IH, uPred_weaken with (S n) x; eauto using cmra_validN_S.
 Qed.
 Lemma later_True' : True ⊑ (▷ True : uPred M).
-Proof. by intros [|n] x. Qed.
+Proof. by split=> -[|n] x. Qed.
 Lemma later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
-Proof. by intros [|n] x; split. Qed.
+Proof. by split=> -[|n] x; split. Qed.
 Lemma later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I.
-Proof. intros [|n] x; simpl; tauto. Qed.
+Proof. split=> -[|n] x; simpl; tauto. Qed.
 Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a)%I ≡ (∀ a, ▷ Φ a)%I.
-Proof. by intros [|n] x. Qed.
+Proof. by split=> -[|n] x. Qed.
 Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊑ (▷ ∃ a, Φ a).
-Proof. by intros [|[|n]] x. Qed.
+Proof. by split=> -[|[|n]] x. Qed.
 Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
   (▷ ∃ a, Φ a)%I ≡ (∃ a, ▷ Φ a)%I.
-Proof. intros [|[|n]] x; split; done || by exists inhabitant; simpl. Qed.
+Proof. split=> -[|[|n]] x; split; done || by exists inhabitant; simpl. Qed.
 Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
 Proof.
-  intros n x ?; split.
+  split=> n x ?; split.
   - destruct n as [|n]; simpl.
     { by exists x, (unit x); rewrite cmra_unit_r. }
     intros (x1&x2&Hx&?&?); destruct (cmra_extend_op n x x1 x2)
@@ -796,6 +828,9 @@ Qed.
 (* Later derived *)
 Global Instance later_mono' : Proper ((⊑) ==> (⊑)) (@uPred_later M).
 Proof. intros P Q; apply later_mono. Qed.
+Global Instance later_flip_mono' :
+  Proper (flip (⊑) ==> flip (⊑)) (@uPred_later M).
+Proof. intros P Q; apply later_mono. Qed.
 Lemma later_True : (▷ True : uPred M)%I ≡ True%I.
 Proof. apply (anti_symm (⊑)); auto using later_True'. Qed.
 Lemma later_impl P Q : ▷ (P → Q) ⊑ (▷ P → ▷ Q).
@@ -825,7 +860,7 @@ Qed.
 Lemma ownM_op (a1 a2 : M) :
   uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
 Proof.
-  intros n x ?; split.
+  split=> n x ?; split.
   - intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
     split. by exists (unit a1); rewrite cmra_unit_r. by exists z.
   - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
@@ -834,28 +869,28 @@ Proof.
 Qed.
 Lemma always_ownM_unit (a : M) : (□ uPred_ownM (unit a))%I ≡ uPred_ownM (unit a).
 Proof.
-  intros n x; split; [by apply always_elim|intros [a' Hx]]; simpl.
+  split=> n x; split; [by apply always_elim|intros [a' Hx]]; simpl.
   rewrite -(cmra_unit_idemp a) Hx.
   apply cmra_unit_preservingN, cmra_includedN_l.
 Qed.
 Lemma always_ownM (a : M) : unit a ≡ a → (□ uPred_ownM a)%I ≡ uPred_ownM a.
 Proof. by intros <-; rewrite always_ownM_unit. Qed.
 Lemma ownM_something : True ⊑ ∃ a, uPred_ownM a.
-Proof. intros n x ??. by exists x; simpl. Qed.
+Proof. split=> n x ??. by exists x; simpl. Qed.
 Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
-Proof. intros n x ??; by  exists x; rewrite left_id. Qed.
+Proof. split=> n x ??; by  exists x; rewrite left_id. Qed.
 
 (* Valid *)
 Lemma ownM_valid (a : M) : uPred_ownM a ⊑ ✓ a.
-Proof. intros n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
+Proof. split=> n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
 Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊑ ✓ a.
-Proof. by intros ? n x ? _; simpl; apply cmra_valid_validN. Qed.
+Proof. by intros ?; split=> n x ? _; simpl; apply cmra_valid_validN. Qed.
 Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊑ False.
-Proof. intros Ha n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
+Proof. intros Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
 Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I.
 Proof. done. Qed.
 Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊑ ✓ a.
-Proof. intros n x _; apply cmra_validN_op_l. Qed.
+Proof. split=> n x _; apply cmra_validN_op_l. Qed.
 
 (* Own and valid derived *)
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
@@ -888,8 +923,8 @@ Lemma timelessP_spec P : TimelessP P ↔ ∀ n x, ✓{n} x → P 0 x → P n x.
 Proof.
   split.
   - intros HP n x ??; induction n as [|n]; auto.
-    by destruct (HP (S n) x); auto using cmra_validN_S.
-  - move=> HP [|n] x /=; auto; left.
+    by destruct (uPred_in_entails _ _ HP (S n) x); auto using cmra_validN_S.
+  - move=> HP; split=> -[|n] x /=; auto; left.
     apply HP, uPred_weaken with n x; eauto using cmra_validN_le.
 Qed.
 Global Instance const_timeless φ : TimelessP (■ φ : uPred M)%I.
@@ -944,7 +979,7 @@ Lemma timeless_eq {A : cofeT} (a b : A) :
   Timeless a → (a ≡ b)%I ≡ (■(a ≡ b) : uPred M)%I.
 Proof.
   intros ?. apply (anti_symm (⊑)).
-  - move=>n x ? ? /=. by apply (timeless_iff n a).
+  - split=> n x ? ? /=. by apply (timeless_iff n a).
   - eapply const_elim; first done. move=>->. apply eq_refl.
 Qed.
 
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index ada372ac10f4b2b28a9094d33fd143cb915e9763..1bce6182c41a918f89ad575eb7a8e56ff408fb70 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -27,7 +27,7 @@ Lemma wp_lift_step E1 E2
     (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E1,E2}=> || e2 @ E2 {{ Φ }} ★ wp_fork ef)
   ⊑ || e1 @ E2 {{ Φ }}.
 Proof.
-  intros ? He Hsafe Hstep n r ? Hvs; constructor; auto.
+  intros ? He Hsafe Hstep; split=> n r ? Hvs; constructor; auto.
   intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1')
     as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'.
   destruct (wsat_update_pst k (E1 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws'].
@@ -36,7 +36,7 @@ Proof.
   constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)].
   destruct (λ H1 H2 H3, Hwp e2 σ2 ef k (update_pst σ2 r1) H1 H2 H3 rf k Ef σ2)
     as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
-  { split. destruct k; try eapply Hstep; eauto. apply ownP_spec; auto. }
+  { split. by eapply Hstep. apply ownP_spec; auto. }
   { rewrite (comm _ r2) -assoc; eauto using wsat_le. }
   by exists r1', r2'; split_and?; [| |by intros ? ->].
 Qed.
@@ -47,7 +47,7 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
   (▷ ∀ e2 ef, ■ φ e2 ef → || e2 @ E {{ Φ }} ★ wp_fork ef) ⊑ || e1 @ E {{ Φ }}.
 Proof.
-  intros He Hsafe Hstep n r ? Hwp; constructor; auto.
+  intros He Hsafe Hstep; split=> n r ? Hwp; constructor; auto.
   intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia.
   intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
   destruct (Hwp e2 ef k r) as (r1&r2&Hr&?&?); auto.
diff --git a/program_logic/model.v b/program_logic/model.v
index 6d4a5d147a8c57a01ee0828189236204195dadf2..1c9ceb17a5205dacd6b591ad7c7402c290bf761c 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -24,8 +24,9 @@ Proof.
     rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
     rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
     by rewrite -later_map_compose.
-  - intros A1 A2 B1 B2 n f f' Hf P n' [???].
-    apply upredC_map_ne, resC_map_ne, laterC_map_contractive=>i. by apply Hf.
+  - intros A1 A2 B1 B2 n f f' Hf P; split=> n' -[???].
+    apply upredC_map_ne, resC_map_ne, laterC_map_contractive.
+    by intros i ?; apply Hf.
 Qed.
 End iProp.
 
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 5ccf36ab2d9dacba8c33606141c5eeb92b8a6d74..9361687002b4de84876fc8607286df17053bf562 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -42,7 +42,7 @@ Transparent uPred_holds.
 
 Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
 Proof.
-  intros P Q HPQ r1 n' ??; simpl; split; intros HP rf k Ef σ ???;
+  intros P Q HPQ; split=> n' r1 ??; simpl; split; intros HP rf k Ef σ ???;
     destruct (HP rf k Ef σ) as (r2&?&?); auto;
     exists r2; split_and?; auto; apply HPQ; eauto.
 Qed.
@@ -51,36 +51,38 @@ Proof. apply ne_proper, _. Qed.
 
 Lemma pvs_intro E P : P ⊑ |={E}=> P.
 Proof.
-  intros n r ? HP rf k Ef σ ???; exists r; split; last done.
+  split=> n r ? HP rf k Ef σ ???; exists r; split; last done.
   apply uPred_weaken with n r; eauto.
 Qed.
 Lemma pvs_mono E1 E2 P Q : P ⊑ Q → (|={E1,E2}=> P) ⊑ (|={E1,E2}=> Q).
 Proof.
-  intros HPQ n r ? HP rf k Ef σ ???.
-  destruct (HP rf k Ef σ) as (r2&?&?); eauto; exists r2; eauto.
+  intros HPQ; split=> n r ? HP rf k Ef σ ???.
+  destruct (HP rf k Ef σ) as (r2&?&?); eauto.
+  exists r2; eauto using uPred_in_entails.
 Qed.
 Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊑ (|={E}=> P).
 Proof.
-  rewrite uPred.timelessP_spec=> HP [|n] r ? HP' rf k Ef σ ???; first lia.
+  rewrite uPred.timelessP_spec=> HP.
+  split=>-[|n] r ? HP' rf k Ef σ ???; first lia.
   exists r; split; last done.
   apply HP, uPred_weaken with n r; eauto using cmra_validN_le.
 Qed.
 Lemma pvs_trans E1 E2 E3 P :
   E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ⊑ (|={E1,E3}=> P).
 Proof.
-  intros ? n r1 ? HP1 rf k Ef σ ???.
+  intros ?; split=> n r1 ? HP1 rf k Ef σ ???.
   destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto.
 Qed.
 Lemma pvs_mask_frame E1 E2 Ef P :
   Ef ∩ (E1 ∪ E2) = ∅ → (|={E1,E2}=> P) ⊑ (|={E1 ∪ Ef,E2 ∪ Ef}=> P).
 Proof.
-  intros ? n r ? HP rf k Ef' σ ???.
+  intros ?; split=> n r ? HP rf k Ef' σ ???.
   destruct (HP rf k (Ef∪Ef') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto.
   by exists r'; rewrite -(assoc_L _).
 Qed.
 Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P) ★ Q) ⊑ (|={E1,E2}=> P ★ Q).
 Proof.
-  intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
+  split; intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
   destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto.
   { by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. }
   exists (r' â‹… r2); split; last by rewrite -assoc.
@@ -88,7 +90,7 @@ Proof.
 Qed.
 Lemma pvs_openI i P : ownI i P ⊑ (|={{[i]},∅}=> ▷ P).
 Proof.
-  intros [|n] r ? Hinv rf [|k] Ef σ ???; try lia.
+  split=> -[|n] r ? Hinv rf [|k] Ef σ ???; try lia.
   apply ownI_spec in Hinv; last auto.
   destruct (wsat_open k Ef σ (r ⋅ rf) i P) as (rP&?&?); auto.
   { rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
@@ -97,7 +99,8 @@ Proof.
 Qed.
 Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ (|={∅,{[i]}}=> True).
 Proof.
-  intros [|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|].
+  split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia.
+  exists ∅; split; [done|].
   rewrite left_id; apply wsat_close with P r.
   - apply ownI_spec, uPred_weaken with (S n) r; auto.
   - set_solver +HE.
@@ -107,7 +110,8 @@ Qed.
 Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
   m ~~>: P → ownG m ⊑ (|={E}=> ∃ m', ■ P m' ∧ ownG m').
 Proof.
-  intros Hup%option_updateP' [|n] r ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
+  intros Hup%option_updateP'.
+  split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia.
   destruct (wsat_update_gst k (E ∪ Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
   { apply cmra_includedN_le with (S n); auto. }
   by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
@@ -116,7 +120,7 @@ Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
     E (P : iGst Λ Σ → Prop) :
   ∅ ~~>: P → True ⊑ (|={E}=> ∃ m', ■ P m' ∧ ownG m').
 Proof.
-  intros Hup [|n] r ? _ rf [|k] Ef σ ???; try lia.
+  intros Hup; split=> -[|n] r ? _ rf [|k] Ef σ ???; try lia.
   destruct (wsat_update_gst k (E ∪ Ef) σ r rf ∅ P) as (m'&?&?); eauto.
   { apply cmra_empty_leastN. }
   { apply cmra_updateP_compose_l with (Some ∅), option_updateP with P;
@@ -125,7 +129,7 @@ Proof.
 Qed.
 Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ (|={E}=> ∃ i, ■ (i ∈ E) ∧ ownI i P).
 Proof.
-  intros ? [|n] r ? HP rf [|k] Ef σ ???; try lia.
+  intros ?; split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia.
   destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
   { apply uPred_weaken with n r; eauto. }
   exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
@@ -137,6 +141,9 @@ Opaque uPred_holds.
 Import uPred.
 Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
 Proof. intros P Q; apply pvs_mono. Qed.
+Global Instance pvs_flip_mono' E1 E2 :
+  Proper (flip (⊑) ==> flip (⊑)) (@pvs Λ Σ E1 E2).
+Proof. intros P Q; apply pvs_mono. Qed.
 Lemma pvs_trans' E P : (|={E}=> |={E}=> P) ⊑ (|={E}=> P).
 Proof. apply pvs_trans; set_solver. Qed.
 Lemma pvs_strip_pvs E P Q : P ⊑ (|={E}=> Q) → (|={E}=> P) ⊑ (|={E}=> Q).
@@ -194,7 +201,6 @@ Proof.
   intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
   by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
 Qed.
-
 End pvs.
 
 (** * Frame Shift Assertions. *)
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 8645e707b774a01cf60fd0fd7815a54dda8fd626..d7e71cc246c216521e318c1c588f9f2497f0c01a 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -162,7 +162,7 @@ Proof. by intros ? ? [???]; constructor; apply: timeless. Qed.
 (** Internalized properties *)
 Lemma res_equivI {M} r1 r2 :
   (r1 ≡ r2)%I ≡ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2: uPred M)%I.
-Proof. split. by destruct 1. by intros (?&?&?); constructor. Qed.
+Proof. do 2 split. by destruct 1. by intros (?&?&?); constructor. Qed.
 Lemma res_validI {M} r : (✓ r)%I ≡ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M)%I.
 Proof. done. Qed.
 End res.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 4ff71923da3025016bd98fc5b60e3cc8673b3a87..ce191a7dd73eae16dbacf8c8631958670a7bcadb 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -71,7 +71,7 @@ Global Instance wp_ne E e n :
 Proof.
   cut (∀ Φ Ψ, (∀ v, Φ v ≡{n}≡ Ψ v) →
     ∀ n' r, n' ≤ n → ✓{n'} r → wp E e Φ n' r → wp E e Ψ n' r).
-  { by intros help Φ Ψ HΦΨ; split; apply help. }
+  { intros help Φ Ψ HΦΨ. by do 2 split; apply help. }
   intros Φ Ψ HΦΨ n' r; revert e r.
   induction n' as [n' IH] using lt_wf_ind=> e r.
   destruct 3 as [n' r v HpvsQ|n' r e1 ? Hgo].
@@ -90,7 +90,8 @@ Qed.
 Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
   E1 ⊆ E2 → (∀ v, Φ v ⊑ Ψ v) → || e @ E1 {{ Φ }} ⊑ || e @ E2 {{ Ψ }}.
 Proof.
-  intros HE HΦ n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
+  intros HE HΦ; split=> n r.
+  revert e r; induction n as [n IH] using lt_wf_ind=> e r.
   destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo].
   { constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
   constructor; [done|]=> rf k Ef σ1 ???.
@@ -114,20 +115,20 @@ Lemma wp_step_inv E Ef Φ e k n σ r rf :
 Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
 
 Lemma wp_value' E Φ v : Φ v ⊑ || of_val v @ E {{ Φ }}.
-Proof. by constructor; apply pvs_intro. Qed.
+Proof. split=> n r; constructor; by apply pvs_intro. Qed.
 Lemma pvs_wp E e Φ : (|={E}=> || e @ E {{ Φ }}) ⊑ || e @ E {{ Φ }}.
 Proof.
-  intros n r ? Hvs.
+  split=> n r ? Hvs.
   destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
   { constructor; eapply pvs_trans', pvs_mono, Hvs; eauto.
-    intros ???; apply wp_value_inv. }
+    split=> ???; apply wp_value_inv. }
   constructor; [done|]=> rf k Ef σ1 ???.
   destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
   eapply wp_step_inv with (S k) r'; eauto.
 Qed.
 Lemma wp_pvs E e Φ : || e @  E {{ λ v, |={E}=> Φ v }} ⊑ || e @ E {{ Φ }}.
 Proof.
-  intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
+  split=> n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
   destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
   { constructor; apply pvs_trans', (wp_value_inv _ (pvs E E ∘ Φ)); auto. }
   constructor; [done|]=> rf k Ef σ1 ???.
@@ -140,7 +141,7 @@ Lemma wp_atomic E1 E2 e Φ :
   E2 ⊆ E1 → atomic e →
   (|={E1,E2}=> || e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) ⊑ || e @ E1 {{ Φ }}.
 Proof.
-  intros ? He n r ? Hvs; constructor; eauto using atomic_not_val.
+  intros ? He; split=> n r ? Hvs; constructor; eauto using atomic_not_val.
   intros rf k Ef σ1 ???.
   destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
   destruct (wp_step_inv E2 Ef (pvs E2 E1 ∘ Φ) e k (S k) σ1 r' rf)
@@ -157,7 +158,7 @@ Proof.
 Qed.
 Lemma wp_frame_r E e Φ R : (|| e @ E {{ Φ }} ★ R) ⊑ || e @ E {{ λ v, Φ v ★ R }}.
 Proof.
-  intros n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
+  split; intros n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
   rewrite Hr; clear Hr; revert e r Hwp.
   induction n as [n IH] using lt_wf_ind; intros e r1.
   destruct 1 as [|n r e ? Hgo]=>?.
@@ -175,7 +176,8 @@ Qed.
 Lemma wp_frame_later_r E e Φ R :
   to_val e = None → (|| e @ E {{ Φ }} ★ ▷ R) ⊑ || e @ E {{ λ v, Φ v ★ R }}.
 Proof.
-  intros He n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid; rewrite Hr; clear Hr.
+  intros He; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
+  revert Hvalid; rewrite Hr; clear Hr.
   destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
   constructor; [done|]=>rf k Ef σ1 ???; destruct n as [|n]; first omega.
   destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep];rewrite ?assoc;auto.
@@ -189,7 +191,7 @@ Qed.
 Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
   || e @ E {{ λ v, || K (of_val v) @ E {{ Φ }} }} ⊑ || K e @ E {{ Φ }}.
 Proof.
-  intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?.
+  split=> n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?.
   destruct 1 as [|n r e ? Hgo]; [by apply pvs_wp|].
   constructor; auto using fill_not_val=> rf k Ef σ1 ???.
   destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.