diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 845eb5ba555120717b3a53c4aa8ddb394b53b432..874fed496af10bf65fd4b8334412805093ba544e 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -631,9 +631,7 @@ Proof. by unseal. Qed.
 
 Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
 Proof.
-  unseal; split=> n x ? /= HPQ. split=> n' x' ??.
-    move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
-    move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
+  unseal; split=> n x ? /=. setoid_rewrite (left_id ε op). split; naive_solver.
 Qed.
 
 (* The following two laws are very similar, and indeed they hold not just for â–¡