diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 629d54ccf1a868be7d7516dce68b536e696217ed..464cb35e6d213729f2527caeffd0192d0ff04fac 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -483,7 +483,12 @@ Lemma always_idemp P : □ □ P ⊣⊢ □ P.
 Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
 
 Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
-Proof. apply (anti_symm _); auto using always_pure_2. Qed.
+Proof.
+  apply (anti_symm _); auto.
+  apply pure_elim'=> Hφ.
+  trans (∀ x : False, □ True : uPred M)%I; [by apply forall_intro|].
+  rewrite always_forall_2. auto using always_mono, pure_intro.
+Qed.
 Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
 Proof.
   apply (anti_symm _); auto using always_forall_2.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 0b84b8d5974fe2ee172c5f76c9e35680a95a6a60..7069ada4878ec08b23c761e38a8a60f9a5dfa5c7 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -430,8 +430,6 @@ Qed.
 Lemma always_idemp_2 P : □ P ⊢ □ □ P.
 Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
 
-Lemma always_pure_2 φ : ⌜φ⌝ ⊢ □ ⌜φ⌝.
-Proof. by unseal. Qed.
 Lemma always_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
 Proof. by unseal. Qed.
 Lemma always_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).