diff --git a/iris/ownership.v b/iris/ownership.v
index 68f99ad9ed2a43029f8a4c980358cfcac86a168f..98bfc972182944ef77c83e3c3644049f84015983 100644
--- a/iris/ownership.v
+++ b/iris/ownership.v
@@ -55,6 +55,8 @@ Proof.
 Qed.
 Lemma ownG_valid m : (ownG m) ⊑ (✓ m).
 Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
+Lemma ownG_valid_r m : (ownG m) ⊑ (ownG m ★ ✓ m).
+Proof. apply uPred.always_entails_r', ownG_valid; by apply _. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
 
diff --git a/iris/viewshifts.v b/iris/viewshifts.v
index a090f5f85fe5109f780a1947396385de47d7de59..79f2e4d46efe29322b5bc5b1aab9d38410fa8aa2 100644
--- a/iris/viewshifts.v
+++ b/iris/viewshifts.v
@@ -19,7 +19,7 @@ Implicit Types P Q : iProp Σ.
 Implicit Types m : iGst Σ.
 Import uPred.
 
-Lemma vs_alt E1 E2 P Q : P ⊑ pvs E1 E2 Q → P >{E1,E2}> Q.
+Lemma vs_alt E1 E2 P Q : (P ⊑ pvs E1 E2 Q) → P >{E1,E2}> Q.
 Proof.
   intros; rewrite -{1}always_const; apply always_intro, impl_intro_l.
   by rewrite always_const (right_id _ _).
diff --git a/modures/logic.v b/modures/logic.v
index a8d29109913dbdf6de2a7fcec86245c8106e4d8e..f3a9a7af05ef812f502916151440ff2e5c019bc1 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -433,6 +433,15 @@ Lemma impl_elim_l' P Q R : P ⊑ (Q → R) → (P ∧ Q) ⊑ R.
 Proof. intros; apply impl_elim with Q; auto. Qed.
 Lemma impl_elim_r' P Q R : Q ⊑ (P → R) → (P ∧ Q) ⊑ R.
 Proof. intros; apply impl_elim with P; auto. Qed.
+Lemma impl_entails P Q : True ⊑ (P → Q) → P ⊑ Q.
+Proof.
+  intros H; eapply impl_elim; last reflexivity. rewrite -H.
+  by apply True_intro.
+Qed.
+Lemma entails_impl P Q : (P ⊑ Q) → True ⊑ (P → Q).
+Proof.
+  intros H; apply impl_intro_l. by rewrite -H and_elim_l.
+Qed.
 
 Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■ φ ∧ Q) ⊑ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
@@ -737,6 +746,26 @@ Proof.
   apply always_intro, impl_intro_r.
   by rewrite always_and_sep_l always_elim wand_elim_l.
 Qed.
+Lemma always_impl_l P Q : (P → □ Q) ⊑ (P → □ Q ★ P).
+Proof.
+  rewrite -always_and_sep_l. apply impl_intro_l, and_intro.
+  - by rewrite impl_elim_r.
+  - by rewrite and_elim_l.
+Qed.
+Lemma always_impl_r P Q : (P → □ Q) ⊑ (P → P ★ □ Q).
+Proof.
+  by rewrite commutative always_impl_l.
+Qed.
+Lemma always_entails_l P Q : (P ⊑ □ Q) → P ⊑ (□ Q ★ P).
+Proof.
+  intros H. apply impl_entails. rewrite -always_impl_l.
+  by apply entails_impl.
+Qed.
+Lemma always_entails_r P Q : (P ⊑ □ Q) → P ⊑ (P ★ □ Q).
+Proof.
+  intros H. apply impl_entails. rewrite -always_impl_r.
+  by apply entails_impl.
+Qed.
 
 (* Own *)
 Lemma own_op (a1 a2 : M) :
@@ -909,4 +938,13 @@ Lemma always_and_sep_r' P Q `{!AlwaysStable Q} : (P ∧ Q)%I ≡ (P ★ Q)%I.
 Proof. by rewrite -(always_always Q) always_and_sep_r. Qed.
 Lemma always_sep_dup' P `{!AlwaysStable P} : P ≡ (P ★ P)%I.
 Proof. by rewrite -(always_always P) -always_sep_dup. Qed.
+Lemma always_impl_l' P Q `{!AlwaysStable Q} : (P → Q) ⊑ (P → Q ★ P).
+Proof. by rewrite -(always_always Q) always_impl_l. Qed.
+Lemma always_impl_r' P Q `{!AlwaysStable Q} : (P → Q) ⊑ (P → P ★ Q).
+Proof. by rewrite -(always_always Q) always_impl_r. Qed.
+Lemma always_entails_l' P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (Q ★ P).
+Proof. by rewrite -(always_always Q); apply always_entails_l. Qed.
+Lemma always_entails_r' P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (P ★ Q).
+Proof. by rewrite -(always_always Q); apply always_entails_r. Qed.
+
 End uPred_logic. End uPred.