diff --git a/algebra/upred.v b/algebra/upred.v
index 73d521139463509343e82842df645fa8ad66e1e9..6072149717cad4add9421669ba4a36eafe5d7a47 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -564,6 +564,8 @@ Proof. intros ->; apply iff_refl. Qed.
 
 Lemma pure_mono Ï†1 Ï†2 : (Ï†1 â†’ Ï†2) â†’ â–  Ï†1 âŠ¢ â–  Ï†2.
 Proof. intros; apply pure_elim with Ï†1; eauto using pure_intro. Qed.
+Lemma pure_iff Ï†1 Ï†2 : (Ï†1 â†” Ï†2) â†’ â–  Ï†1 âŠ£âŠ¢ â–  Ï†2.
+Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
 Lemma and_mono P P' Q Q' : (P âŠ¢ Q) â†’ (P' âŠ¢ Q') â†’ P âˆ§ P' âŠ¢ Q âˆ§ Q'.
 Proof. auto. Qed.
 Lemma and_mono_l P P' Q : (P âŠ¢ Q) â†’ P âˆ§ P' âŠ¢ Q âˆ§ P'.