diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index 41342f5abe278f3cc8c1a36f0504984c5f9e3b94..0000000000000000000000000000000000000000
--- a/.gitmodules
+++ /dev/null
@@ -1,3 +0,0 @@
-[submodule "autosubst"]
-	path = autosubst
-	url = https://github.com/tebbi/autosubst.git
diff --git a/_CoqProject b/_CoqProject
index 799dd63084571ea5bd46def5c08053611bc1dce0..2495807aaf749e8dda63ab0a197f6ab833bed2e6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,2 +1 @@
 -Q . ""
--R autosubst/theories Autosubst
diff --git a/autosubst b/autosubst
deleted file mode 160000
index 07c669460cd84e6e0b2084e870b19f947b699ded..0000000000000000000000000000000000000000
--- a/autosubst
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 07c669460cd84e6e0b2084e870b19f947b699ded
diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index f67a22da5c0d6db82acce3404ed8a884ec77696e..9dfcbf9cdb31369556aeb987da4654ca2275a1b2 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -1,7 +1,5 @@
 Require Import Autosubst.Autosubst.
-Require Import prelude.option prelude.gmap iris.language iris.parameter.
-
-Set Bullet Behavior "Strict Subproofs".
+Require Import prelude.option prelude.gmap iris.parameter.
 
 (** Some tactics useful when dealing with equality of sigma-like types: existT T0 t0 = existT T1 t1.
     They all assume such an equality is the first thing on the "stack" (goal). *)
diff --git a/iris/adequacy.v b/iris/adequacy.v
new file mode 100644
index 0000000000000000000000000000000000000000..5d89cf9315a80575b88277593b4c86d7f070c529
--- /dev/null
+++ b/iris/adequacy.v
@@ -0,0 +1,110 @@
+Require Export iris.hoare.
+Require Import iris.wsat.
+Local Hint Extern 10 (_ ≤ _) => omega.
+Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
+Local Hint Extern 10 (✓{_} _) =>
+  repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
+  solve_validN.
+
+Section adequacy.
+Context {Σ : iParam}.
+Implicit Types e : iexpr Σ.
+Implicit Types Q : ival Σ → iProp Σ.
+Transparent uPred_holds.
+
+Notation wptp n := (Forall3 (λ e Q r, uPred_holds (wp coPset_all e Q) n r)).
+Lemma wptp_le Qs es rs n n' :
+  ✓{n'} (big_op rs) → wptp n es Qs rs → n' ≤ n → wptp n' es Qs rs.
+Proof. induction 2; constructor; eauto using uPred_weaken. Qed.
+Lemma nsteps_wptp Qs k n tσ1 tσ2 rs1 :
+  nsteps step k tσ1 tσ2 →
+  1 < n → wptp (k + n) (tσ1.1) Qs rs1 →
+  wsat (k + n) coPset_all (tσ1.2) (big_op rs1) →
+  ∃ rs2 Qs', wptp n (tσ2.1) (Qs ++ Qs') rs2 ∧
+             wsat n coPset_all (tσ2.2) (big_op rs2).
+Proof.
+  intros Hsteps Hn; revert Qs rs1.
+  induction Hsteps as [|k ?? tσ3 [e1 σ1 e2 σ2 ef t1 t2 ?? Hstep] Hsteps IH];
+    simplify_equality'; intros Qs rs.
+  { by intros; exists rs, []; rewrite right_id_L. }
+  intros (Qs1&?&rs1&?&->&->&?&
+    (Q&Qs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?.
+  destruct (wp_step_inv coPset_all ∅ Q e1 (k + n) (S (k + n)) σ1 r
+    (big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using values_stuck.
+  { by rewrite right_id_L -big_op_cons Permutation_middle. }
+  destruct (Hwpstep e2 σ2 ef) as (r2&r2'&Hwsat&?&?); auto; clear Hwpstep.
+  revert Hwsat; rewrite big_op_app right_id_L=>Hwsat.
+  destruct ef as [e'|].
+  * destruct (IH (Qs1 ++ Q :: Qs2 ++ [λ _, True%I])
+      (rs1 ++ r2 :: rs2 ++ [r2'])) as (rs'&Qs'&?&?).
+    { apply Forall3_app, Forall3_cons,
+        Forall3_app, Forall3_cons, Forall3_nil; eauto using wptp_le. }
+    { by rewrite -Permutation_middle /= (associative (++))
+        (commutative (++)) /= associative big_op_app. }
+    exists rs', ([λ _, True%I] ++ Qs'); split; auto.
+    by rewrite (associative _ _ _ Qs') -(associative _ Qs1).
+  * apply (IH (Qs1 ++ Q :: Qs2) (rs1 ++ r2 â‹… r2' :: rs2)).
+    { rewrite /option_list right_id_L.
+      apply Forall3_app, Forall3_cons; eauto using wptp_le.
+      apply uPred_weaken with r2 (k + n); eauto using @ra_included_l. }
+    by rewrite -Permutation_middle /= big_op_app.
+Qed.
+Lemma ht_adequacy_steps P Q k n e1 t2 σ1 σ2 r1 :
+  {{ P }} e1 @ coPset_all {{ Q }} →
+  nsteps step k ([e1],σ1) (t2,σ2) →
+  1 < n → wsat (k + n) coPset_all σ1 r1 →
+  P (k + n) r1 →
+  ∃ rs2 Qs', wptp n t2 ((λ v, pvs coPset_all coPset_all (Q v)) :: Qs') rs2 ∧
+             wsat n coPset_all σ2 (big_op rs2).
+Proof.
+  intros Hht ????; apply (nsteps_wptp [pvs coPset_all coPset_all ∘ Q] k n
+    ([e1],σ1) (t2,σ2) [r1]); rewrite /big_op ?right_id; auto.
+  constructor; last constructor.
+  apply Hht with r1 (k + n); eauto using @ra_included_unit.
+  by destruct (k + n).
+Qed.
+Theorem ht_adequacy_result E φ e v t2 σ1 σ2 :
+  {{ ownP σ1 }} e @ E {{ λ v', ■ φ v' }} →
+  rtc step ([e], σ1) (of_val v :: t2, σ2) →
+  φ v.
+Proof.
+  intros ? [k ?]%rtc_nsteps.
+  destruct (ht_adequacy_steps (ownP σ1) (λ v', ■ φ v')%I k 2 e
+    (of_val v :: t2) σ1 σ2 (Res ∅ (Excl σ1) ∅)) as (rs2&Qs&Hwptp&?); auto.
+  { by rewrite -(ht_mask_weaken E coPset_all). }
+  { rewrite Nat.add_comm; apply wsat_init. }
+  { by rewrite /uPred_holds /=. }
+  inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
+  apply wp_value_inv in Hwp; destruct (Hwp (big_op rs) 2 ∅ σ2) as [r' []]; auto.
+  by rewrite right_id_L.
+Qed.
+Lemma ht_adequacy_reducible E Q e1 e2 t2 σ1 σ2 :
+  {{ ownP σ1 }} e1 @ E {{ Q }} →
+  rtc step ([e1], σ1) (t2, σ2) →
+  e2 ∈ t2 → to_val e2 = None → reducible e2 σ2.
+Proof.
+  intros ? [k ?]%rtc_nsteps [i ?]%elem_of_list_lookup He.
+  destruct (ht_adequacy_steps (ownP σ1) Q k 3 e1
+    t2 σ1 σ2 (Res ∅ (Excl σ1) ∅)) as (rs2&Qs&?&?); auto.
+  { by rewrite -(ht_mask_weaken E coPset_all). }
+  { rewrite Nat.add_comm; apply wsat_init. }
+  { by rewrite /uPred_holds /=. }
+  destruct (Forall3_lookup_l (λ e Q r, wp coPset_all e Q 3 r) t2
+    (pvs coPset_all coPset_all ∘ Q :: Qs) rs2 i e2) as (Q'&r2&?&?&Hwp); auto.
+  destruct (wp_step_inv coPset_all ∅ Q' e2 2 3 σ2 r2 (big_op (delete i rs2)));
+    rewrite ?right_id_L ?big_op_delete; auto.
+Qed.
+Theorem ht_adequacy_safe E Q e1 t2 σ1 σ2 :
+  {{ ownP σ1 }} e1 @ E {{ Q }} →
+  rtc step ([e1], σ1) (t2, σ2) →
+  Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
+Proof.
+  intros.
+  destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
+  apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
+  destruct (ht_adequacy_reducible E Q e1 e2 t2 σ1 σ2) as (e3&σ3&ef&?);
+    rewrite ?eq_None_not_Some; auto.
+  destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
+  right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
+Qed.
+End adequacy.
diff --git a/iris/hoare_lifting.v b/iris/hoare_lifting.v
index dac04e964595b4081270c80e33c22dece7745958..53886aab2687164483c8d3d52300af421d651885 100644
--- a/iris/hoare_lifting.v
+++ b/iris/hoare_lifting.v
@@ -15,7 +15,7 @@ Import uPred.
 Lemma ht_lift_step E1 E2
     (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P P' Q1 Q2 R e1 σ1 :
   E1 ⊆ E2 → to_val e1 = None →
-  (∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
   (P >{E2,E1}> (ownP σ1 ★ ▷ P') ∧ ∀ e2 σ2 ef,
     (■ φ e2 σ2 ef ★ ownP σ2 ★ P') >{E1,E2}> (Q1 e2 σ2 ef ★ Q2 e2 σ2 ef) ∧
@@ -45,7 +45,7 @@ Qed.
 Lemma ht_lift_atomic E
     (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P e1 σ1 :
   atomic e1 →
-  (∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
   (∀ e2 σ2 ef, {{ ■ φ e2 σ2 ef ★ P }} ef ?@ coPset_all {{ λ _, True }}) ⊑
   {{ ownP σ1 ★ ▷ P }} e1 @ E {{ λ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}.
@@ -71,7 +71,7 @@ Proof.
 Qed.
 Lemma ht_lift_pure_step E (φ : iexpr Σ → option (iexpr Σ) → Prop) P P' Q e1 :
   to_val e1 = None →
-  (∀ σ1, ∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
   (∀ e2 ef,
     {{ ■ φ e2 ef ★ P }} e2 @ E {{ Q }} ∧
@@ -97,7 +97,7 @@ Qed.
 Lemma ht_lift_pure_determistic_step E
     (φ : iexpr Σ → option (iexpr Σ) → Prop) P P' Q e1 e2 ef :
   to_val e1 = None →
-  (∀ σ1, prim_step e1 σ1 e2 σ1 ef) →
+  (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
   ({{ P }} e2 @ E {{ Q }} ∧ {{ P' }} ef ?@ coPset_all {{ λ _, True }})
   ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Q }}.
diff --git a/iris/language.v b/iris/language.v
index 525ffd4a9190ff638692b892730b129c73c2ac3b..09c9aee60741e217cb7bb73cf17f86bf8dca1bce 100644
--- a/iris/language.v
+++ b/iris/language.v
@@ -19,6 +19,11 @@ Arguments Build_Language {_ _ _} _ _ _ _ {_ _ _ _ _}.
 Section language.
   Context `{Language E V St}.
 
+  Definition reducible (e : E) (σ : St) :=
+    ∃ e' σ' ef, prim_step e σ e' σ' ef.
+  Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
+  Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
+
   Lemma atomic_of_val v : ¬atomic (of_val v).
   Proof.
     by intros Hat; apply atomic_not_value in Hat; rewrite to_of_val in Hat.
@@ -30,13 +35,10 @@ Section language.
   Inductive step (ρ1 ρ2 : cfg) : Prop :=
     | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
-       ρ1 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
+       ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
        prim_step e1 σ1 e2 σ2 ef →
        step ρ1 ρ2.
 
-  Definition steps := rtc step.
-  Definition stepn := nsteps step.
-
   Record is_ctx (K : E → E) := IsCtx {
     is_ctx_value e : to_val e = None → to_val (K e) = None;
     is_ctx_step_preserved e1 σ1 e2 σ2 ef :
diff --git a/iris/lifting.v b/iris/lifting.v
index 8526f16e4ed5c1f40b3be94613969edee30fa107..c94eda289e988da9ac0c8ea2dd2298a147a9437d 100644
--- a/iris/lifting.v
+++ b/iris/lifting.v
@@ -16,7 +16,7 @@ Transparent uPred_holds.
 Lemma wp_lift_step E1 E2
     (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) Q e1 σ1 :
   E1 ⊆ E2 → to_val e1 = None →
-  (∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
   pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ∧ ownP σ2) -★
     pvs E1 E2 (wp E2 e2 Q ★ default True ef (flip (wp coPset_all) (λ _, True))))
@@ -37,7 +37,7 @@ Proof.
 Qed.
 Lemma wp_lift_pure_step E (φ : iexpr Σ → option (iexpr Σ) → Prop) Q e1 :
   to_val e1 = None →
-  (∀ σ1, ∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
   (▷ ∀ e2 ef, ■ φ e2 ef →
     wp E e2 Q ★ default True ef (flip (wp coPset_all) (λ _, True)))
diff --git a/iris/parameter.v b/iris/parameter.v
index 66a71493cf75d0d9aa6729a4c114c2578821f04f..cfbf73ee39c65de9138adace5faa06ee88e87e32 100644
--- a/iris/parameter.v
+++ b/iris/parameter.v
@@ -1,7 +1,5 @@
 Require Export modures.cmra iris.language.
 
-Set Bullet Behavior "Strict Subproofs".
-
 Record iParam := IParam {
   iexpr : Type;
   ival : Type;
@@ -29,6 +27,8 @@ Proof.
   by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
 Qed.
 
+Canonical Structure istateC Σ := leibnizC (istate Σ).
+
 Definition IParamConst {iexpr ival istate : Type}
            (ilanguage : Language iexpr ival istate)
            (icmra : cmraT) {icmra_empty : Empty icmra}
@@ -39,5 +39,3 @@ Unshelve.
 - by intros.
 - by intros.
 Defined.
-
-Canonical Structure istateC Σ := leibnizC (istate Σ).
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index 3e34864facf61be6f6578060083622cb1563ce06..3e9a5088b8266b24a59103ce360de16eb1a1d020 100644
--- a/iris/weakestpre.v
+++ b/iris/weakestpre.v
@@ -9,7 +9,7 @@ Local Hint Extern 10 (✓{_} _) =>
 
 Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → res' Σ → Prop)
     (k : nat) (rf : res' Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
-  wf_safe : ∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef;
+  wf_safe : reducible e1 σ1;
   wp_step e2 σ2 ef :
     prim_step e1 σ1 e2 σ2 ef →
     ∃ r2 r2',
@@ -83,6 +83,17 @@ Proof.
   by intros Q Q' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
 
+Lemma wp_value_inv E Q v n r : wp E (of_val v) Q n r → Q v n r.
+Proof.
+  inversion 1 as [| |??? He]; simplify_equality; auto.
+  by rewrite ?to_of_val in He.
+Qed.
+Lemma wp_step_inv E Ef Q e k n σ r rf :
+  to_val e = None → 1 < k < n → E ∩ Ef = ∅ →
+  wp E e Q n r → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) →
+  wp_go (E ∪ Ef) (λ e, wp E e Q) (λ e, wp coPset_all e (λ _, True%I)) k rf e σ.
+Proof. intros He; destruct 3; [lia|by rewrite ?to_of_val in He|eauto]. Qed.
+
 Lemma wp_value E Q v : Q v ⊑ wp E (of_val v) Q.
 Proof. by constructor. Qed.
 Lemma wp_mono E e Q1 Q2 : (∀ v, Q1 v ⊑ Q2 v) → wp E e Q1 ⊑ wp E e Q2.
@@ -91,9 +102,7 @@ Lemma wp_pvs E e Q : pvs E E (wp E e Q) ⊑ wp E e (λ v, pvs E E (Q v)).
 Proof.
   intros r [|n] ?; [done|]; intros Hvs.
   destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
-  { constructor; eapply pvs_mono, Hvs; auto; clear.
-    intros r n ?; inversion 1 as [| |??? He]; simplify_equality; auto.
-    by rewrite ?to_of_val in He. }
+  { by constructor; eapply pvs_mono, Hvs; [intros ???; apply wp_value_inv|]. }
   constructor; [done|intros rf k Ef σ1 ???].
   destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
   inversion Hwp as [| |???? Hgo]; subst; [by rewrite to_of_val in He|].
diff --git a/iris/wsat.v b/iris/wsat.v
index 598d20786458ec615300ddf9c58e97c378f54548..ac5f7e5019d34b59c08b3779ef48d9d1489b3f82 100644
--- a/iris/wsat.v
+++ b/iris/wsat.v
@@ -63,6 +63,14 @@ Proof.
   destruct n; [intros; apply cmra_valid_0|intros [rs ?]].
   eapply cmra_valid_op_l, wsat_pre_valid; eauto.
 Qed.
+Lemma wsat_init k E σ : wsat (S k) E σ (Res ∅ (Excl σ) ∅).
+Proof.
+  exists ∅; constructor; auto.
+  * rewrite big_opM_empty right_id.
+    split_ands'; try (apply cmra_valid_validN, ra_empty_valid); constructor.
+  * by intros i; rewrite lookup_empty=>-[??].
+  * intros i P ?; rewrite /= (left_id _ _) lookup_empty; inversion_clear 1.
+Qed.
 Lemma wsat_open n E σ r i P :
   wld r !! i ={S n}= Some (to_agree (Later (iProp_unfold P))) → i ∉ E →
   wsat (S n) ({[i]} ∪ E) σ r → ∃ rP, wsat (S n) E σ (rP ⋅ r) ∧ P n rP.
diff --git a/modures/ra.v b/modures/ra.v
index bfc324de4ece896dcd375cc1e8c7b4193c9a0b88..4401556a103147cac4987d9922a35fda7972e785 100644
--- a/modures/ra.v
+++ b/modures/ra.v
@@ -125,6 +125,10 @@ Lemma ra_empty_least x : ∅ ≼ x.
 Proof. by exists x; rewrite (left_id _ _). Qed.
 
 (** * Big ops *)
+Lemma big_op_nil : big_op (@nil A) = ∅.
+Proof. done. Qed.
+Lemma big_op_cons x xs : big_op (x :: xs) = x â‹… big_op xs.
+Proof. done. Qed.
 Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
 Proof.
   induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
@@ -147,6 +151,9 @@ Proof.
   * by transitivity (big_op ys); [|apply ra_included_r].
   * by transitivity (big_op ys).
 Qed.
+Lemma big_op_delete xs i x :
+  xs !! i = Some x → x ⋅ big_op (delete i xs) ≡ big_op xs.
+Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.
 
 Context `{FinMap K M}.
 Lemma big_opM_empty : big_opM (∅ : M A) ≡ ∅.
diff --git a/prelude/list.v b/prelude/list.v
index 6e0bac82ae30832c2582a686ab64310422c5be2d..ef167dc392dd8dbcd7307416bb4e333f26e57bc4 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -1372,6 +1372,11 @@ Proof.
   induction l as [|x l IH]; [done|].
   by rewrite reverse_cons, (commutative (++)), IH.
 Qed.
+Lemma delete_Permutation l i x : l !! i = Some x → l ≡ₚ x :: delete i l.
+Proof.
+  revert i; induction l as [|y l IH]; intros [|i] ?; simplify_equality'; auto.
+  by rewrite Permutation_swap, <-(IH i).
+Qed.
 
 (** ** Properties of the [prefix_of] and [suffix_of] predicates *)
 Global Instance: PreOrder (@prefix_of A).
@@ -2522,59 +2527,85 @@ End Forall2_order.
 Section Forall3.
   Context {A B C} (P : A → B → C → Prop).
   Hint Extern 0 (Forall3 _ _ _ _) => constructor.
-  Lemma Forall3_app l1 k1 k1' l2 k2 k2' :
+  Lemma Forall3_app l1 l2 k1 k2 k1' k2' :
     Forall3 P l1 k1 k1' → Forall3 P l2 k2 k2' →
     Forall3 P (l1 ++ l2) (k1 ++ k2) (k1' ++ k2').
   Proof. induction 1; simpl; auto. Qed.
-  Lemma Forall3_cons_inv_m l y l2' k :
-    Forall3 P l (y :: l2') k → ∃ x l2 z k2,
-      l = x :: l2 ∧ k = z :: k2 ∧ P x y z ∧ Forall3 P l2 l2' k2.
+  Lemma Forall3_cons_inv_l x l k k' :
+    Forall3 P (x :: l) k k' → ∃ y k2 z k2',
+      k = y :: k2 ∧ k' = z :: k2' ∧ P x y z ∧ Forall3 P l k2 k2'.
+  Proof. inversion_clear 1; naive_solver. Qed.
+  Lemma Forall3_app_inv_l l1 l2 k k' :
+    Forall3 P (l1 ++ l2) k k' → ∃ k1 k2 k1' k2',
+     k = k1 ++ k2 ∧ k' = k1' ++ k2' ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
+  Proof.
+    revert k k'. induction l1 as [|x l1 IH]; simpl; inversion_clear 1.
+    * by repeat eexists; eauto.
+    * by repeat eexists; eauto.
+    * edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
+  Qed.
+  Lemma Forall3_cons_inv_m l y k k' :
+    Forall3 P l (y :: k) k' → ∃ x l2 z k2',
+      l = x :: l2 ∧ k' = z :: k2' ∧ P x y z ∧ Forall3 P l2 k k2'.
+  Proof. inversion_clear 1; naive_solver. Qed.
+  Lemma Forall3_app_inv_m l k1 k2 k' :
+    Forall3 P l (k1 ++ k2) k' → ∃ l1 l2 k1' k2',
+     l = l1 ++ l2 ∧ k' = k1' ++ k2' ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
+  Proof.
+    revert l k'. induction k1 as [|x k1 IH]; simpl; inversion_clear 1.
+    * by repeat eexists; eauto.
+    * by repeat eexists; eauto.
+    * edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
+  Qed.
+  Lemma Forall3_cons_inv_r l k z k' :
+    Forall3 P l k (z :: k') → ∃ x l2 y k2,
+      l = x :: l2 ∧ k = y :: k2 ∧ P x y z ∧ Forall3 P l2 k2 k'.
   Proof. inversion_clear 1; naive_solver. Qed.
-  Lemma Forall3_app_inv_m l l1' l2' k :
-    Forall3 P l (l1' ++ l2') k → ∃ l1 l2 k1 k2,
-      l = l1 ++ l2 ∧ k = k1 ++ k2 ∧ Forall3 P l1 l1' k1 ∧ Forall3 P l2 l2' k2.
+  Lemma Forall3_app_inv_r l k k1' k2' :
+    Forall3 P l k (k1' ++ k2') → ∃ l1 l2 k1 k2,
+      l = l1 ++ l2 ∧ k = k1 ++ k2 ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
   Proof.
-    revert l k. induction l1' as [|x l1' IH]; simpl; inversion_clear 1.
+    revert l k. induction k1' as [|x k1' IH]; simpl; inversion_clear 1.
     * by repeat eexists; eauto.
     * by repeat eexists; eauto.
     * edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
   Qed.
-  Lemma Forall3_impl (Q : A → B → C → Prop) l l' k :
-    Forall3 P l l' k → (∀ x y z, P x y z → Q x y z) → Forall3 Q l l' k.
-  Proof. intros Hl ?. induction Hl; auto. Defined.
-  Lemma Forall3_length_lm l l' k : Forall3 P l l' k → length l = length l'.
+  Lemma Forall3_impl (Q : A → B → C → Prop) l k k' :
+    Forall3 P l k k' → (∀ x y z, P x y z → Q x y z) → Forall3 Q l k k'.
+  Proof. intros Hl ?; induction Hl; auto. Defined.
+  Lemma Forall3_length_lm l k k' : Forall3 P l k k' → length l = length k.
   Proof. by induction 1; f_equal'. Qed.
-  Lemma Forall3_length_lr l l' k : Forall3 P l l' k → length l = length k.
+  Lemma Forall3_length_lr l k k' : Forall3 P l k k' → length l = length k'.
   Proof. by induction 1; f_equal'. Qed.
-  Lemma Forall3_lookup_lmr l l' k i x y z :
-    Forall3 P l l' k →
-    l !! i = Some x → l' !! i = Some y → k !! i = Some z → P x y z.
+  Lemma Forall3_lookup_lmr l k k' i x y z :
+    Forall3 P l k k' →
+    l !! i = Some x → k !! i = Some y → k' !! i = Some z → P x y z.
   Proof.
     intros H. revert i. induction H; intros [|?] ???; simplify_equality'; eauto.
   Qed.
-  Lemma Forall3_lookup_l l l' k i x :
-    Forall3 P l l' k → l !! i = Some x →
-    ∃ y z, l' !! i = Some y ∧ k !! i = Some z ∧ P x y z.
+  Lemma Forall3_lookup_l l k k' i x :
+    Forall3 P l k k' → l !! i = Some x →
+    ∃ y z, k !! i = Some y ∧ k' !! i = Some z ∧ P x y z.
   Proof.
     intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
   Qed.
-  Lemma Forall3_lookup_m l l' k i y :
-    Forall3 P l l' k → l' !! i = Some y →
-    ∃ x z, l !! i = Some x ∧ k !! i = Some z ∧ P x y z.
+  Lemma Forall3_lookup_m l k k' i y :
+    Forall3 P l k k' → k !! i = Some y →
+    ∃ x z, l !! i = Some x ∧ k' !! i = Some z ∧ P x y z.
   Proof.
     intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
   Qed.
-  Lemma Forall3_lookup_r l l' k i z :
-    Forall3 P l l' k → k !! i = Some z →
-    ∃ x y, l !! i = Some x ∧ l' !! i = Some y ∧ P x y z.
+  Lemma Forall3_lookup_r l k k' i z :
+    Forall3 P l k k' → k' !! i = Some z →
+    ∃ x y, l !! i = Some x ∧ k !! i = Some y ∧ P x y z.
   Proof.
     intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
   Qed.
-  Lemma Forall3_alter_lm f g l l' k i :
-    Forall3 P l l' k →
-    (∀ x y z, l !! i = Some x → l' !! i = Some y → k !! i = Some z →
+  Lemma Forall3_alter_lm f g l k k' i :
+    Forall3 P l k k' →
+    (∀ x y z, l !! i = Some x → k !! i = Some y → k' !! i = Some z →
       P x y z → P (f x) (g y) z) →
-    Forall3 P (alter f i l) (alter g i l') k.
+    Forall3 P (alter f i l) (alter g i k) k'.
   Proof. intros Hl. revert i. induction Hl; intros [|]; auto. Qed.
 End Forall3.