diff --git a/algebra/upred.v b/algebra/upred.v
index a8ce1ad7bfa318da757bf633021e0cadedb8d75b..f18d8e31b2e3d9cfc0bb1408c9aed95302223ec2 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -670,6 +670,8 @@ Proof.
   apply wand_intro_l. rewrite ![(_ ★ P)%I]comm -assoc.
   apply sep_mono_r, wand_elim_r.
 Qed.
+Lemma wand_diag P : (P -★ P)%I ≡ True%I.
+Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
 Lemma sep_and P Q : (P ★ Q) ⊑ (P ∧ Q).
 Proof. auto. Qed.
 Lemma impl_wand P Q : (P → Q) ⊑ (P -★ Q).