diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v
index 89694ad76a8803c3c55a6ab24cd789c2f8a02fa3..acb593a057b290bc18ae775b8d1237da261f7373 100644
--- a/algebra/upred_tactics.v
+++ b/algebra/upred_tactics.v
@@ -122,14 +122,14 @@ Module uPred_reflection. Section uPred_reflection.
   Qed.
   Lemma split_l Σ e l k :
     remove_all l (flatten e) = Some k →
-    eval Σ e ≡ eval Σ (ESep (to_expr l) (to_expr k)).
+    eval Σ e ≡ (eval Σ (to_expr l) ★ eval Σ (to_expr k))%I.
   Proof.
     intros He%remove_all_permutation.
-    by rewrite eval_flatten He fmap_app big_sep_app /= !eval_to_expr.
+    by rewrite eval_flatten He fmap_app big_sep_app !eval_to_expr.
   Qed.
   Lemma split_r Σ e l k :
     remove_all l (flatten e) = Some k →
-    eval Σ e ≡ eval Σ (ESep (to_expr k) (to_expr l)).
+    eval Σ e ≡ (eval Σ (to_expr k) ★ eval Σ (to_expr l))%I.
   Proof. intros. rewrite /= comm. by apply split_l. Qed.
 
   Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.