diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v
index 280a6d36b5d44f1f87444a040d7bbf1799fed112..547c9c53a53bbf305082204d4cd7afe41f93ab05 100644
--- a/iris/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -198,7 +198,7 @@ Section language.
   Proof.
     intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=.
     move: Ht; rewrite -Permutation_middle (symmetry_iff (≡ₚ)).
-    intros (tl'&tr'&->&Ht)%Permutation_cons_inv.
+    intros (tl'&tr'&->&Ht)%Permutation_cons_inv_r.
     exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
     by rewrite -!Permutation_middle !assoc_L Ht.
   Qed.