diff --git a/opam b/opam
index 74cfc66fde788612585c24cfce76e7dc36aa8143..042694642ea8dc0486d44755cd4d5e77cec6790c 100644
--- a/opam
+++ b/opam
@@ -12,5 +12,5 @@ remove: ["sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'"]
 depends: [
   "coq" { >= "8.6.1" & < "8.8~" }
   "coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2017-09-21.2") | (= "dev") }
+  "coq-stdpp" { (= "dev.2017-09-24.0") | (= "dev") }
 ]
diff --git a/opam.pins b/opam.pins
index 7034b445798280e7b05ccc6b0c8caa5190eef4b8..6bdd007ff49f2f199807d04a4c5b682c9d31fae6 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 2f9f3d3f28aa568f5cbee1be5699f163800491c0
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 4ea9c34a9c58a13aae97b4cc7f75fc862bdfcc7c
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index a4e9cf07933d516c239bd298ab8afe48b54e6628..6dc76129cd13ff94f38a4515e042f4e69286545c 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -83,4 +83,14 @@ Section language.
   Lemma irreducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → irreducible e σ → irreducible (K e) σ.
   Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
+
+  Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
+    t1 ≡ₚ t1' → step (t1,σ1) (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) (t2',σ2).
+  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.
+    exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
+    by rewrite -!Permutation_middle !assoc_L Ht.
+  Qed.
 End language.