diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 38178d2197b4229ce458adf308718d9ce39313d0..c0d87d3e067b977e78271e43af148bce892c3d53 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -96,13 +96,11 @@ Qed.
 
 Lemma ht_frame_l E P Φ R e :
   {{ P }} e @ E {{ Φ }} ⊢ {{ R ★ P }} e @ E {{ v, R ★ Φ v }}.
-Proof.
-  iIntros "#Hwp ! [HR HP]". iApply wp_frame_l; iFrame "HR". by iApply "Hwp".
-Qed.
+Proof. iIntros "#Hwp ! [$ HP]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_r E P Φ R e :
   {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ R }} e @ E {{ v, Φ v ★ R }}.
-Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
+Proof. iIntros "#Hwp ! [HP $]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
index 30ebfd256a4b1ccb912d0284c5c110a1127fb2fd..2e60cd40e9d4d4b24fedff69edd140ceafa25fac 100644
--- a/proofmode/weakestpre.v
+++ b/proofmode/weakestpre.v
@@ -8,6 +8,9 @@ Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 
+Global Instance frame_wp E e R Φ Ψ :
+  (∀ v, Frame R (Φ v) (Ψ v)) → Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
+Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 Global Instance fsa_split_wp E e Φ :
   FSASplit (WP e @ E {{ Φ }})%I E (wp_fsa e) (language.atomic e) Φ.
 Proof. split. done. apply _. Qed.