diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 84346a0a095f8e860fe3c57343105cc5c1fb06a5..4fa4299a1a3d0c278af18fe6e8c540f760124ad2 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -107,18 +107,15 @@ Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
 Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
   ((R1 ={E1,E2}=> ▷ R2) ∧ (R2 ={E2,E1}=> R3) ∧ {{ P }} e @ E {{ Φ }})
-    ⊢ {{ R1 ★ P }} e @ (E ∪ E1) {{ λ v, R3 ★ Φ v }}.
+    ⊢ {{ R1 ★ P }} e @ E ∪ E1 {{ λ v, R3 ★ Φ v }}.
 Proof.
   iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]".
   iApply (wp_frame_step_l E E1 E2); try done.
-  iSplitL "HR".
-  - (* TODO: Is there a way to do "apply Hvs1 in Hr"? *)
-    iPvs "Hvs1" "HR"; first by set_solver.
-    (* TODO: iApply pvs_intro? *)
-    rewrite -pvs_intro.
-    iNext. iPvs "Hvs2" "Hvs1"; first by set_solver.
-    rewrite -pvs_intro. done.
-  - iApply "Hwp". done.
+  iSplitL "HR"; [|by iApply "Hwp"].
+  iPvs "Hvs1" "HR"; first by set_solver.
+  iPvsIntro. iNext.
+  iPvs "Hvs2" "Hvs1"; first by set_solver.
+  by iPvsIntro.
 Qed.
 
 Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
@@ -128,8 +125,7 @@ Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
 Proof.
   iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]]".
   setoid_rewrite (comm _ _ R3).
-  iApply ht_frame_step_l; try eassumption. iSplit; last iSplit;
-     iIntros "!"; done.
+  iApply ht_frame_step_l; try eassumption. repeat iSplit; by iIntros "!".
 Qed.
 
 Lemma ht_frame_step_l' E P R e Φ :
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 93beb81c08013624af946a339e01037673c1b31a..6d576bd4b57d2399ea17dd0cc8a31a6be5fae1c2 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -198,33 +198,37 @@ Proof.
 Qed.
 Lemma wp_frame_step_r E E1 E2 e Φ R :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
-  (WP e @ E {{ Φ }} ★ |={E1,E2}=> ▷ |={E2,E1}=> R)
-  ⊢ WP e @ (E ∪ E1) {{ v, Φ v ★ R }}.
+    (WP e @ E {{ Φ }} ★ |={E1,E2}=> ▷ |={E2,E1}=> R)
+  ⊢ WP e @ E ∪ E1 {{ v, Φ v ★ R }}.
+Proof.
   rewrite wp_eq pvs_eq=> He ??.
   uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&HR); cofe_subst.
   constructor; [done|]=>rf k Ef σ1 ?? Hws1.
   destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
   (* "execute" HR *)
-  edestruct (HR (r ⋅ rf) (S k) (E ∪ Ef) σ1) as [s [Hvs Hws2]]; [omega|set_solver| |].
-  { eapply wsat_change, Hws1; first by set_solver+.
-    rewrite assoc [rR â‹… _]comm. done. } clear Hws1 HR.
+  destruct (HR (r ⋅ rf) (S k) (E ∪ Ef) σ1) as (s&Hvs&Hws2); auto.
+  { eapply wsat_proper, Hws1; first by set_solver+.
+    by rewrite assoc [rR â‹… _]comm. }
+  clear Hws1 HR.
   (* Take a step *)
-  destruct (Hgo (s⋅rf) k (E2 ∪ Ef) σ1) as [Hsafe Hstep]; [done|set_solver| |].
-  { eapply wsat_change, Hws2; first by set_solver+.
-    rewrite !assoc [s â‹… _]comm. done. } clear Hgo.
+  destruct (Hgo (s⋅rf) k (E2 ∪ Ef) σ1) as [Hsafe Hstep]; auto.
+  { eapply wsat_proper, Hws2; first by set_solver+.
+    by rewrite !assoc [s â‹… _]comm. }
+  clear Hgo.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&Hws3&?&?); auto. clear Hws2.
   (* Execute 2nd part of the view shift *)
-  edestruct (Hvs (r2 ⋅ r2' ⋅ rf) k (E ∪ Ef) σ2) as [t [HR Hws4]]; [omega|set_solver| |].
-  { eapply wsat_change, Hws3; first by set_solver+.
-    rewrite !assoc [_ â‹… s]comm !assoc. done. } clear Hvs Hws3.
+  destruct (Hvs (r2 ⋅ r2' ⋅ rf) k (E ∪ Ef) σ2) as (t&HR&Hws4); auto.
+  { eapply wsat_proper, Hws3; first by set_solver+.
+    by rewrite !assoc [_ â‹… s]comm !assoc. }
+  clear Hvs Hws3.
   (* Execute the rest of e *)
   exists (r2 â‹… t), r2'. split_and?; auto.
-  - eapply wsat_change, Hws4; first by set_solver+.
-    rewrite !assoc [_ â‹… t]comm. done.
-  - rewrite -uPred_sep_eq. move:(wp_frame_r). rewrite wp_eq=>Hframe.
+  - eapply wsat_proper, Hws4; first by set_solver+.
+    by rewrite !assoc [_ â‹… t]comm.
+  - rewrite -uPred_sep_eq. move: wp_frame_r. rewrite wp_eq=>Hframe.
     apply Hframe; first by auto. uPred.unseal; exists r2, t; split_and?; auto.
-    move:(wp_mask_frame_mono). rewrite wp_eq=>Hmask.
+    move: wp_mask_frame_mono. rewrite wp_eq=>Hmask.
     eapply (Hmask E); by auto.
 Qed.
 Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index c08a73ce50357da3d433a71af1938f37d10ee165..a7d4a2ffc7ec9ad884d18c3ddadbb2599d8c0aaf 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -42,11 +42,11 @@ Proof.
 Qed.
 Global Instance wsat_ne n : Proper (dist n ==> iff) (@wsat Λ Σ n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed.
-Global Instance wsat_proper n : Proper ((≡) ==> iff) (@wsat Λ Σ n E σ) | 1.
+Global Instance wsat_proper' n : Proper ((≡) ==> iff) (@wsat Λ Σ n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed.
-Lemma wsat_change n E1 E2 σ r1 r2 :
+Lemma wsat_proper n E1 E2 σ r1 r2 :
   E1 = E2 → r1 ≡ r2 → wsat n E1 σ r1 → wsat n E2 σ r2.
-Proof. move=>->->. done. Qed.
+Proof. by move=>->->. Qed.
 Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r.
 Proof.
   destruct n as [|n], n' as [|n']; simpl; try by (auto with lia).