diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v
index 9605b0c36aeae163b43c9b0dc56669f543cbbfb3..5e7e2fb2ea6e8a36f0b8b070eaa028df15607f49 100644
--- a/algebra/upred_tactics.v
+++ b/algebra/upred_tactics.v
@@ -117,6 +117,10 @@ Module upred_reflection. Section upred_reflection.
     end.
 End upred_reflection.
 
+Tactic Notation "solve_sep_entails" :=
+  upred_reflection.quote; apply upred_reflection.flatten_entails;
+  apply (bool_decide_unpack _); vm_compute; exact Logic.I.
+
 Tactic Notation "cancel" constr(Ps) :=
   upred_reflection.quote;
   match goal with