Steps are preserved by permutations.

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") }
 ]

opam.pins

-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 2f9f3d3f28aa568f5cbee1be5699f163800491c0
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 4ea9c34a9c58a13aae97b4cc7f75fc862bdfcc7c

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.