diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 7161b21..953c12b 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -11,14 +11,14 @@ jobs:
     - uses: cachix/install-nix-action@v24
       with:
         github_access_token: ${{ secrets.GITHUB_TOKEN }}
-    - run: nix build .#coq-artifact
+    - run: nix build .#rocq-artifact
 
   build:
     runs-on: ubuntu-latest
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:8.20'
+          - 'rocq/rocq-prover:9.2'
       max-parallel: 4
       fail-fast: false
 
diff --git a/Makefile b/Makefile
index ac8dba0..a709cd9 100644
--- a/Makefile
+++ b/Makefile
@@ -22,7 +22,7 @@ clean: Makefile.coq
 
 # Create Coq Makefile.
 Makefile.coq: _CoqProject Makefile
-	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
+	"$(COQBIN)rocq" makefile -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
 # Install build-dependencies
 OPAMFILES=$(wildcard *.opam)
diff --git a/flake.nix b/flake.nix
index 1cb8c0e..abb3d63 100644
--- a/flake.nix
+++ b/flake.nix
@@ -1,7 +1,7 @@
 {
   description = "gitrees";
   inputs = {
-    nixpkgs.url = github:NixOS/nixpkgs/nixos-24.11;
+    nixpkgs.url = github:NixOS/nixpkgs/nixos-26.05;
     flake-utils.url = github:numtide/flake-utils;
   };
   outputs = { self, nixpkgs, flake-utils }:
@@ -9,26 +9,26 @@
       let
         pkgs = nixpkgs.legacyPackages.${system};
         lib = pkgs.lib;
-        coq = pkgs.coq_8_20;
-        coqPkgs = pkgs.coqPackages_8_20;
+        rocq = pkgs.rocq-core_9_2;
+        rocqPkgs = pkgs.rocqPackages_9_2;
       in {
         packages = {
-          coq-artifact = coqPkgs.mkCoqDerivation {
-            pname = "coq-artifact";
+          rocq-artifact = rocqPkgs.mkRocqDerivation {
+            pname = "rocq-artifact";
             version = "main";
             src = ./.;
             buildPhase = "make";
             propagatedBuildInputs = [
-              coqPkgs.stdpp
-              coqPkgs.iris
+              rocqPkgs.stdpp
+              rocqPkgs.iris
             ];
           };
         };
         devShell = pkgs.mkShell {
           buildInputs = with pkgs; [
-            coq
+            rocq
           ];
-          inputsFrom = [ self.packages.${system}.coq-artifact ];
+          inputsFrom = [ self.packages.${system}.rocq-artifact ];
         };
       });
 }
diff --git a/theories/effects/callcc.v b/theories/effects/callcc.v
index 06e610b..0d91515 100644
--- a/theories/effects/callcc.v
+++ b/theories/effects/callcc.v
@@ -15,30 +15,33 @@ Program Definition throwE : opInterp :=
 
 Definition contE := @[callccE;throwE].
 
-Definition reify_callcc X `{Cofe X} : ((laterO X -n> laterO X) -n> laterO X) *
+Definition reify_callcc X `{!Cofe X} : ((laterO X -n> laterO X) -n> laterO X) *
                                         unitO * (laterO X -n> laterO X) →
                                       option (laterO X * unitO * listO (laterO X)) :=
   λ '(f, σ, k), Some ((k (f k): laterO X), σ : unitO, []).
-#[export] Instance reify_callcc_ne X `{Cofe X} :
+#[export] Instance reify_callcc_ne X `{!Cofe X} :
   NonExpansive (reify_callcc X :
     prodO (prodO ((laterO X -n> laterO X) -n> laterO X) unitO)
       (laterO X -n> laterO X) →
     optionO ((laterO X) * unitO * listO (laterO X))%type).
 Proof. intros ?[[]][[]][[]]. simpl in *. repeat f_equiv; auto. Qed.
 
-Definition reify_throw X `{Cofe X} :
+Definition reify_throw X `{!Cofe X} :
   ((laterO X * (laterO (X -n> X))) * unitO * (Empty_setO -n> laterO X)) →
   option (laterO X * unitO * listO (laterO X)) :=
   λ '((e, k'), σ, _),
     Some (((laterO_ap k' : laterO X -n> laterO X) e : laterO X), σ : unitO, []).
-#[export] Instance reify_throw_ne X `{Cofe X} :
+#[export] Instance reify_throw_ne X `{!Cofe X} :
   NonExpansive (reify_throw X :
       prodO (prodO (prodO (laterO X) (laterO (X -n> X))) unitO)
         (Empty_setO -n> laterO X) →
     optionO ((laterO X) * (unitO) * listO (laterO X))%type).
 Proof.
-  intros ?[[[]]][[[]]]?. rewrite /reify_throw.
-  repeat f_equiv; apply H0.
+  intros n [[[e1 k1] []] h1] [[[e2 k2] []] h2] [[[He Hk] _] _].
+  rewrite /reify_throw /=.
+  do 3 f_equiv.
+  etrans; first exact (later_ap_ne n k1 k2 Hk e1).
+  apply (later_ap k2). exact He.
 Qed.
 
 Program Canonical Structure reify_cont : sReifier CtxDep :=
diff --git a/theories/effects/coroutines.v b/theories/effects/coroutines.v
index 15f0561..000b70c 100644
--- a/theories/effects/coroutines.v
+++ b/theories/effects/coroutines.v
@@ -1,7 +1,7 @@
 (** Coroutines effects *)
 From iris.algebra Require Import gmap excl auth gmap_view list.
-From iris.proofmode Require Import classes tactics.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import classes proofmode.
+From iris.bi Require Import algebra cmra.
 From iris.heap_lang Require Export locations.
 From gitrees Require Import prelude gitree hom.
 
@@ -92,7 +92,7 @@ Proof.
   apply Next_contractive.
   destruct n; first apply dist_later_0.
   apply dist_later_S.
-  f_equiv; first (apply Hp; lia).
+  f_equiv; first (apply Hp; apply SIdx.lt_succ_diag_r).
   apply (compose (proj2 (dist_later_S _ _ _)) (later_car_anti_contractive (S n) (_ q1) (_ q2))).
   by f_equiv.
 Qed.
@@ -382,7 +382,7 @@ Section program_logic.
     iDestruct (auth_both_validI with "J") as "((%c & #J1) & J2)".
     rewrite /op /cmra_op /= /excl_op_instance /= /ucmra_op /=.
     iRewrite "J1" in "J2".
-    iDestruct (uPred.cmra_valid_elim with "J2") as "%J".
+    iDestruct (internal_cmra_valid_elim with "J2") as "%J".
     destruct c as [[c|] |].
     - iExFalso.
       iPureIntro.
@@ -733,9 +733,9 @@ Section lib.
     reflexivity.
   Qed.
   Local Instance REC_val body : IntoVal (REC body) (RECV body).
-  Proof.
+  Proof using CR R n rs Σ.
     rewrite /IntoVal.
-    apply bi.siProp.internal_eq_soundness.
+    apply (@bi.internal_eq.internal_eq_soundness iProp _).
     iLöb as "IH".
     iEval (rewrite REC_unfold RECV_unfold).
     iApply f_equivI.
diff --git a/theories/effects/exceptions.v b/theories/effects/exceptions.v
index 8d11bf2..9f09b1f 100644
--- a/theories/effects/exceptions.v
+++ b/theories/effects/exceptions.v
@@ -68,13 +68,13 @@ Module Exc (Errors : ExcSig).
   Definition exceptE := @[regE;popE;throwE].
   
   (** Register a handler : Push the handler and current context on the stack **)
-  Definition reify_reg X `{Cofe X} :
+  Definition reify_reg X `{!Cofe X} :
     excO * (laterO X -n> laterO X) * (laterO X)
     * (stateF ♯ X) * (laterO X -n> laterO X) →
     option (laterO X * (stateF ♯ X) * listO (laterO X)) :=
       λ '(e, h, b, σ, k), Some (b, (e,h,k)::σ, []).
   
-  #[export] Instance reify_reg_ne X `{Cofe X}
+  #[export] Instance reify_reg_ne X `{!Cofe X}
     : NonExpansive (reify_reg X : excO * (laterO X -n> laterO X)
                                   * (laterO X) * (stateF ♯ X) * (laterO X -n> laterO X)
                                   → option (laterO X * (stateF ♯ X) * listO (laterO X))).
@@ -82,13 +82,13 @@ Module Exc (Errors : ExcSig).
     solve_proper_prepare.
     destruct x as [[[[? ?] ?] ?] ?].
     destruct y as [[[[? ?] ?] ?] ?].
-      repeat rewrite e pair_dist in H0.
-      destruct H0 as [[[[? ?] ?] ?] ?].
+      repeat rewrite e pair_dist in H.
+      destruct H as [[[[? ?] ?] ?] ?].
       repeat f_equiv; done.
   Qed.
   
   (** Unregister a handler : Remove the topmost handler, restore the ambient context from when it was registered **)
-  Definition reify_pop X `{Cofe X} :
+  Definition reify_pop X `{!Cofe X} :
     excO * (stateF ♯ X) * (unitO -n> laterO X)
     → option (laterO X * (stateF ♯ X) * listO (laterO X)) :=
     λ '(err, σ, k), match σ with
@@ -99,7 +99,7 @@ Module Exc (Errors : ExcSig).
                          else None)
                     end.
   
-  #[export] Instance reify_pop_ne X `{Cofe X} :
+  #[export] Instance reify_pop_ne X `{!Cofe X} :
     NonExpansive (reify_pop X :
         excO * (stateF ♯ X) * (unitO -n> laterO X)
         → option (laterO X * (stateF ♯ X) * listO (laterO X))).
@@ -200,7 +200,7 @@ Module Exc (Errors : ExcSig).
   Qed.
   
   (** Raise an error : Find the most recent handler handling this error and remove all handlers registered after it from the stack then invoke the handler inside the context from when it was registered **)
-  Definition reify_throw X `{Cofe X} :
+  Definition reify_throw X `{!Cofe X} :
     (excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X)
     → option (laterO X * (stateF ♯ X) * listO (laterO X)) :=
     λ '(x, σ, _), let (err,v) := x in
@@ -209,15 +209,15 @@ Module Exc (Errors : ExcSig).
                   | Some (_, h, k, σ') => Some (k (h v), σ', [])
                   end.
   
-  #[export] Instance reify_throw_ne X `{Cofe X} :
+  #[export] Instance reify_throw_ne X `{!Cofe X} :
     NonExpansive (reify_throw X :
         (excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X)
         → option (laterO X * (stateF ♯ X) * listO (laterO X))).
   Proof.
-    solve_proper_prepare.
+    intros n x y Hxy.
     destruct x as [[[e v] σ] k].
     destruct y as [[[e' v'] σ'] k'].
-    destruct H0 as [[[He Hv] Hσ] Hk].
+    destruct Hxy as [[[He Hv] Hσ] Hk].
     simpl in *.
     generalize dependent σ'.
     induction σ as [|[[err hand] kont] σ].
diff --git a/theories/effects/fork.v b/theories/effects/fork.v
index 59da554..3614108 100644
--- a/theories/effects/fork.v
+++ b/theories/effects/fork.v
@@ -15,10 +15,10 @@ Program Definition forkI : opInterp :=
 Definition concE := @[forkI].
 
 (* FORK *)
-Definition reify_fork' X `{Cofe X} : (laterO X) * stateO →
+Definition reify_fork' X `{!Cofe X} : (laterO X) * stateO →
                                       option (unitO * stateO * listO (laterO X)) :=
     λ '(o, σ), Some ((), σ, [o]).
-#[export] Instance reify_fork'_ne X `{Cofe X} :
+#[export] Instance reify_fork'_ne X `{!Cofe X} :
   NonExpansive (reify_fork' X).
 Proof.
   intros ?[? []] [? []] G.
diff --git a/theories/effects/io_tape.v b/theories/effects/io_tape.v
index 111585a..aa92375 100644
--- a/theories/effects/io_tape.v
+++ b/theories/effects/io_tape.v
@@ -34,10 +34,10 @@ Program Definition outputE : opInterp :=
 Definition ioE := @[inputE;outputE].
 
 (* INPUT *)
-Definition reify_input X `{Cofe X} : unitO * stateO →
+Definition reify_input X `{!Cofe X} : unitO * stateO →
                                       option (natO * stateO * listO (laterO X)) :=
     λ '(o, σ), Some (update_input σ : prodO natO stateO, []).
-#[export] Instance reify_input_ne X `{Cofe X} :
+#[export] Instance reify_input_ne X `{!Cofe X} :
   NonExpansive (reify_input X).
 Proof.
   intros ?[[]][[]][_?]. simpl in *. f_equiv.
@@ -45,10 +45,10 @@ Proof.
 Qed.
 
 (* OUTPUT *)
-Definition reify_output X `{Cofe X} : (natO * stateO) →
+Definition reify_output X `{!Cofe X} : (natO * stateO) →
                                        option (unitO * stateO * listO (laterO X)) :=
   λ '(n, σ), Some((), update_output n σ : stateO, []).
-#[export] Instance reify_output_ne X `{Cofe X} :
+#[export] Instance reify_output_ne X `{!Cofe X} :
   NonExpansive (reify_output X).
 Proof.
   intros ?[][][]. simpl in *.
diff --git a/theories/effects/store.v b/theories/effects/store.v
index 037ed80..dbe8ef4 100644
--- a/theories/effects/store.v
+++ b/theories/effects/store.v
@@ -1,7 +1,7 @@
 (** Higher-order store effect *)
 From iris.algebra Require Import gmap excl auth gmap_view list.
-From iris.proofmode Require Import classes tactics.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import classes proofmode.
+From iris.bi Require Import algebra.
 From iris.heap_lang Require Export locations.
 From gitrees Require Import prelude.
 From gitrees Require Import gitree.
@@ -36,7 +36,7 @@ Lemma gen_fresh_slice_val {A} (σ : gmap loc A) p a x y :
 Proof.
   induction p as [| ? IH].
   - simpl; intros H; inversion H.
-  - simpl; intros [H | H%elem_of_list_singleton]%elem_of_app;
+  - simpl; intros [H | H%list_elem_of_singleton]%elem_of_app;
       first by apply IH.
     by inversion H; subst.
 Qed.
@@ -49,9 +49,9 @@ Proof.
   - simpl; intros H.
     rewrite fmap_app in H.
     apply elem_of_app in H.
-    destruct H as [H | ->%elem_of_list_singleton].
+    destruct H as [H | ->%list_elem_of_singleton].
     + by apply elem_of_app; left; apply IH.
-    + by apply elem_of_app; right; simpl; apply elem_of_list_singleton.
+    + by apply elem_of_app; right; simpl; apply list_elem_of_singleton.
 Qed.
 
 Lemma gen_fresh_slice_no_dup {A} (σ : gmap loc A) p a :
@@ -67,13 +67,13 @@ Proof.
   simpl; apply NoDup_app.
   split; first done.
   split; last apply NoDup_singleton.
-  intros x H ->%elem_of_list_singleton.
+  intros x H ->%list_elem_of_singleton.
   assert (∀ i : nat, (Loc.fresh (dom σ) +ₗ (p + i)%nat, a) ∉ gen_fresh_slice σ p a) as J.
   {
     clear.
     induction p as [| ? IH].
     - set_solver.
-    - simpl; intros i [H | H%elem_of_list_singleton]%elem_of_app.
+    - simpl; intros i [H | H%list_elem_of_singleton]%elem_of_app.
       + rewrite -PeanoNat.Nat.add_succ_r in H.
         by apply (IH (S i)).
       + inversion H as [J]; subst.
@@ -218,8 +218,8 @@ Proof.
       * apply dist_later_0.
       * apply dist_later_S.
         do 2 f_equiv.
-        -- apply Hk; lia.
-        -- apply Hxy; lia.
+        -- apply Hk; apply SIdx.lt_succ_diag_r.
+        -- apply Hxy; apply SIdx.lt_succ_diag_r.
     + rewrite !later_map_Next.
       rewrite Hm.
       f_equiv; last done.
@@ -228,8 +228,8 @@ Proof.
       -- apply dist_later_0.
       -- apply dist_later_S.
          do 2 f_equiv.
-         ++ apply Hk; lia.
-         ++ apply Hxy; lia.
+         ++ apply Hk; apply SIdx.lt_succ_diag_r.
+         ++ apply Hxy; apply SIdx.lt_succ_diag_r.
   - by rewrite Hp Hm.
 Qed.
 
@@ -919,14 +919,14 @@ Section wp.
             * apply dist_later_0.
             * apply dist_later_S.
               f_equiv.
-              apply H; lia.
+              apply H; apply SIdx.lt_succ_diag_r.
           + do 2 f_equiv.
             apply Next_contractive.
             destruct m.
             * apply dist_later_0.
             * apply dist_later_S.
               f_equiv.
-              apply H; lia.
+              apply H; apply SIdx.lt_succ_diag_r.
         - done.
       }
       {
@@ -1110,14 +1110,14 @@ Module xchg_wp.
               * apply dist_later_0.
               * apply dist_later_S.
                 f_equiv.
-                apply H; lia.
+                apply H; apply SIdx.lt_succ_diag_r.
             + do 2 f_equiv.
               apply Next_contractive.
               destruct m.
               * apply dist_later_0.
               * apply dist_later_S.
                 f_equiv.
-                apply H; lia.
+                apply H; apply SIdx.lt_succ_diag_r.
           - done.
         }
         {
diff --git a/theories/examples/affine_lang/logrel2.v b/theories/examples/affine_lang/logrel2.v
index ff983d2..f6e31a0 100644
--- a/theories/examples/affine_lang/logrel2.v
+++ b/theories/examples/affine_lang/logrel2.v
@@ -408,7 +408,7 @@ Section glue.
     iClear "Hl". clear l.
     iApply fupd_wp.
     { solve_proper. }
-    iMod (inv_alloc (nroot.@"yolo") _ (∃ n, pointsto l' (Ret n)) with "[Hl']") as "#Hinv".
+    iMod (inv_alloc (nroot.@"yolo") _ (∃ n : natO, pointsto l' (Ret n : IT)) with "[Hl']") as "#Hinv".
     { iNext. iExists _; done. }
     iPoseProof ("Ha" $! (thunkedV (IT_of_V β'v) l') with "[-Has]") as "H1".
     {
@@ -422,7 +422,7 @@ Section glue.
                 (⊤∖ nclose (nroot.@"storeE")) _ _ _ idfun with "Hctx").
       { set_solver. }
       iInv (nroot.@"yolo") as (n) "Hl'" "Hcl".
-      iModIntro. iExists (Ret n). iFrame.
+      iModIntro. iExists (Ret n : IT). iFrame.
       iNext. iNext. iIntros "Hl'".
       iMod ("Hcl" with "[Hl']") as "_".
       { iNext. eauto with iFrame. }
diff --git a/theories/examples/delim_lang/example.v b/theories/examples/delim_lang/example.v
index 3709892..c1645c9 100644
--- a/theories/examples/delim_lang/example.v
+++ b/theories/examples/delim_lang/example.v
@@ -3,8 +3,8 @@ From gitrees Require Import gitree lang_generic.
 From gitrees.effects Require Import delim store.
 From gitrees.lib Require Import pairs.
 From gitrees.examples.delim_lang Require Import lang interp.
-From iris.proofmode Require Import base classes tactics environments.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import base classes proofmode environments.
+From iris.bi Require Import algebra.
 
 Open Scope syn_scope.
 
diff --git a/theories/examples/delim_lang/glue.v b/theories/examples/delim_lang/glue.v
index 2fd3408..6dede4a 100644
--- a/theories/examples/delim_lang/glue.v
+++ b/theories/examples/delim_lang/glue.v
@@ -4,8 +4,8 @@ From gitrees.effects Require Import delim store.
 From gitrees.examples.delim_lang Require Import lang interp typing hom .
 From gitrees.utils Require Import clwp wbwp.
 From iris.algebra Require Import list gmap.
-From iris.proofmode Require Import base classes tactics environments.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import base classes proofmode environments.
+From iris.bi Require Import algebra.
 From iris.heap_lang Require Import locations.
 Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env.
 
@@ -518,14 +518,18 @@ Section sets.
     iIntros (γ) "#Hγ".
     iSpecialize ("H" $! γ with "Hγ").
     iClear "Hγ".
-    unshelve eset (K := MkHom (λne v, interp_alloc (R := R) rs (constO v) γ) _ : HOM).
-    1-2: apply _.
+    pose (store_subEff :=
+      @subEffCtxIndep sz CtxDep rs reify_store subReifier1).
+    unshelve epose (alloc_ctx :=
+      ((λne v, @ALLOC F store_subEff R CR v (@Ret F locO R CR SubOfe2)) : IT -n> IT)).
     { solve_proper. }
-    { simpl; apply _. }
-    { apply _. }
+    pose (K := MkHom (LETCTX alloc_ctx) (LETCTX_Hom alloc_ctx) : HOM).
     assert ((interp_expr rs (Alloc e) γ)
               ≡ K (interp_expr rs e γ))%stdpp as ->.
-    { reflexivity. }
+    {
+      subst K alloc_ctx store_subEff; unfold interp_alloc, LETCTX; simpl.
+      f_equiv; intro; reflexivity.
+    }
     iApply interp_exprG_bind.
     iApply (interp_exprG_mono with "H"); iClear "H".
     iIntros (w) "#H".
@@ -654,15 +658,16 @@ Section sets.
     iIntros (γ) "#Hγ".
     iSpecialize ("H" $! γ with "Hγ").
     iClear "Hγ".
-    unshelve eset (K := MkHom
-                          (λne v, interp_deref (R := R) rs (constO v) γ) _ : HOM).
-    1-2: apply _.
-    { solve_proper. }
-    { simpl; apply _. }
-    { apply _. }
+    pose (read_ctx := ((λne l : loc, READ l) : locO -n> IT)).
+    assert (read_ctx_hom : IT_hom (get_ret read_ctx)).
+    { unfold get_ret; apply _. }
+    pose (K := MkHom (get_ret read_ctx) read_ctx_hom : HOM).
     assert ((interp_expr rs (Deref e) γ)
               ≡ K (interp_expr rs e γ))%stdpp as ->.
-    { reflexivity. }
+    {
+      subst K; unfold interp_deref; simpl.
+      apply get_ret_proper; intro; reflexivity.
+    }
     iApply interp_exprG_bind.
     iApply (interp_exprG_mono with "H"); iClear "H".
     iIntros (v) "#H".
@@ -753,9 +758,7 @@ Section sets.
       iAssert (NATOP (do_natop op) (IT_of_V w) (Ret n)
                  ≡ NATOP (do_natop op) (Ret n') (Ret n))%I as "#HEQ2'''".
       {
-        unshelve iApply (f_equivI (λne x, NATOP (do_natop op) x (Ret n))).
-        { solve_proper. }
-        { solve_proper. }
+        iApply (f_equivI (NatOpLSCtx (do_natop op) (Ret n))).
         iApply "HEQ2''".
       }
       iRewrite "HEQ2'''".
@@ -1110,8 +1113,7 @@ Proof.
           simpl in Hr.
           rewrite -Hr.
           reflexivity.
-        - iExFalso. iApply (IT_ret_fun_ne).
-          iExact "J1".
+        - iExFalso. iApply (IT_ret_fun_ne n' f with "J1").
       }
       iPureIntro.
       rewrite Hfoo.
diff --git a/theories/examples/delim_lang/interp.v b/theories/examples/delim_lang/interp.v
index 43614ff..38ebc9b 100644
--- a/theories/examples/delim_lang/interp.v
+++ b/theories/examples/delim_lang/interp.v
@@ -3,8 +3,8 @@ From gitrees Require Import gitree lang_generic.
 From gitrees.effects Require Import delim.
 From gitrees.examples.delim_lang Require Import lang.
 From iris.algebra Require Import list.
-From iris.proofmode Require Import classes tactics.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import classes proofmode.
+From iris.bi Require Import algebra.
 
 Require Import Binding.Lib Binding.Set.
 
@@ -355,7 +355,7 @@ Section interp.
   Global Instance ArrEquiv {A B : Set} : Equiv (A [→] B) :=
     fun f g => ∀ x, f x = g x.
 
-  Global Instance ArrDist {A B : Set} `{Dist B} : Dist (A [→] B) :=
+  Global Instance ArrDist {A B : Set} `{!Dist B} : Dist (A [→] B) :=
     fun n => fun f g => ∀ x, f x ≡{n}≡ g x.
 
   Global Instance ren_scope_proper {S S'} :
@@ -394,7 +394,7 @@ Section interp.
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_ren.
-        apply bi.siProp.internal_eq_soundness.
+        apply (@bi.internal_eq.internal_eq_soundness siProp _).
         iLöb as "IH".
         rewrite {2}interp_rec_unfold.
         rewrite {2}(interp_rec_unfold (interp_expr e)).
@@ -479,7 +479,7 @@ Section interp.
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_subst.
-        apply bi.siProp.internal_eq_soundness.
+        apply (@bi.internal_eq.internal_eq_soundness siProp _).
         iLöb as "IH".
         rewrite {2}interp_rec_unfold.
         rewrite {2}(interp_rec_unfold (interp_expr e)).
diff --git a/theories/examples/delim_lang/logpred.v b/theories/examples/delim_lang/logpred.v
index ea41f85..1f405d0 100644
--- a/theories/examples/delim_lang/logpred.v
+++ b/theories/examples/delim_lang/logpred.v
@@ -3,8 +3,8 @@ From gitrees Require Import gitree lang_generic hom.
 From gitrees.effects Require Import delim.
 From gitrees.examples.delim_lang Require Import lang interp typing hom.
 From iris.algebra Require Import list.
-From iris.proofmode Require Import classes tactics.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import classes proofmode.
+From iris.bi Require Import algebra.
 
 Require Import Binding.Lib Binding.Set Binding.Env.
 
@@ -432,12 +432,9 @@ Section logrel.
       rewrite IT_of_V_Ret.
       iAssert (NATOP (do_natop op) (IT_of_V v) (Ret n)
                  ≡ NATOP (do_natop op) (Ret n') (Ret n))%I as "#HEQ2''".
-      {
-        unshelve iApply (f_equivI (λne x, NATOP (do_natop op) x (Ret n))).
-        { solve_proper. }
-        { solve_proper. }
-        iApply "HEQ2'".
-      }
+      { iRewrite "HEQ2".
+        rewrite (IT_of_V_Ret n').
+        done. }
       iRewrite - "HEQ2''".
       done.
     }
@@ -793,7 +790,9 @@ Proof.
     iIntros "#Hαv %F %Q Hs Hss".
     iApply ("Hs" with "Hαv Hss").
   }
-  iSpecialize ("Hlog" $! [] with "[]").
+  unfold 𝒫_HOM. simpl.
+  subst st.
+  iSpecialize ("Hlog" $! [] (λne _, True%I) with "[] Hs").
   {
     iIntros (αv) "HHH GGG".
     iApply (wp_pop_end with "GGG").
@@ -801,15 +800,9 @@ Proof.
     iIntros "_ GGG".
     iApply wp_val.
     iModIntro.
-    iFrame "HHH GGG".
+    done.
   }
-  subst st.
-  iSpecialize ("Hlog" with "Hs").
-  simpl.
-  iApply (wp_wand with "Hlog").
-  iIntros (βv). simpl.
-  iIntros "_".
-  done.
+  iApply "Hlog".
 Qed.
 
 Lemma safety e σ (β : IT (sReifier_ops (gReifiers_sReifier rs)) natO) k :
diff --git a/theories/examples/delim_lang/logrel.v b/theories/examples/delim_lang/logrel.v
index 9ec30b7..50078a3 100644
--- a/theories/examples/delim_lang/logrel.v
+++ b/theories/examples/delim_lang/logrel.v
@@ -3,8 +3,8 @@ From gitrees Require Import gitree lang_generic hom.
 From gitrees.effects Require Import delim.
 From gitrees.examples.delim_lang Require Import lang interp typing hom.
 From iris.algebra Require Import list.
-From iris.proofmode Require Import classes tactics.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import classes proofmode.
+From iris.bi Require Import algebra.
 
 Require Import Binding.Lib Binding.Set Binding.Env.
 
@@ -648,9 +648,7 @@ Section logrel.
           iAssert (NATOP (do_natop op) (IT_of_V v) (Ret n)
                      ≡ NATOP (do_natop op) (Ret n') (Ret n))%I as "#HEQ2'''".
           {
-            unshelve iApply (f_equivI (λne x, NATOP (do_natop op) x (Ret n))).
-            { solve_proper. }
-            { solve_proper. }
+            iApply (f_equivI (NatOpLSCtx (do_natop op) (Ret n))).
             iApply "HEQ2''".
           }
           iRewrite "HEQ2'''".
@@ -1223,7 +1221,7 @@ Proof.
   iAssert (True%I) as "G"; first done; iFrame "G"; iClear "G".
   iModIntro. iSplitL ""; last first.
   - iIntros "Hst HΦ Hstuck".
-    iAssert ((IT_to_V (Ret n)) ≡ Some (RetV n))%I as "HEQ".
+    iAssert ((IT_to_V (Ret n : IT (gReifiers_ops rs) natO)) ≡ Some (RetV n))%I as "HEQ".
     { by rewrite IT_to_V_Ret. }
     iDestruct (internal_eq_rewrite _ _
                  (λ x, from_option Φ True%I x)
diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v
index 092442a..6784c69 100644
--- a/theories/examples/except_lang/interp.v
+++ b/theories/examples/except_lang/interp.v
@@ -459,7 +459,7 @@ Module interp (Errors : ExcSig).
     Global Instance ArrEquiv {A B : Set} : Equiv (A [→] B) :=
       fun f g => ∀ x, f x = g x.
 
-    Global Instance ArrDist {A B : Set} `{Dist B} : Dist (A [→] B) :=
+    Global Instance ArrDist {A B : Set} `{!Dist B} : Dist (A [→] B) :=
       fun n => fun f g => ∀ x, f x ≡{n}≡ g x.
 
     Global Instance ren_scope_proper {S S'} :
@@ -496,7 +496,7 @@ Module interp (Errors : ExcSig).
       - destruct e; simpl.
         + reflexivity.
         + clear -interp_expr_ren.
-          apply bi.siProp.internal_eq_soundness.
+          apply (@bi.internal_eq.internal_eq_soundness siProp _).
           iLöb as "IH".
           rewrite {2}interp_rec_unfold.
           rewrite {2}(interp_rec_unfold (interp_expr e)).
@@ -561,7 +561,7 @@ Module interp (Errors : ExcSig).
       - destruct e; simpl.
         + reflexivity.
         + clear -interp_expr_subst.
-          apply bi.siProp.internal_eq_soundness.
+          apply (@bi.internal_eq.internal_eq_soundness siProp _).
           iLöb as "IH".
           rewrite {2}interp_rec_unfold.
           rewrite {2}(interp_rec_unfold (interp_expr e)).
diff --git a/theories/examples/heap_lang/metatheory.v b/theories/examples/heap_lang/metatheory.v
index 7217d32..1f15d5f 100644
--- a/theories/examples/heap_lang/metatheory.v
+++ b/theories/examples/heap_lang/metatheory.v
@@ -155,7 +155,7 @@ Proof.
     { eapply heap_array_map_disjoint;
         rewrite length_replicate Z2Nat.id; auto with lia. }
     destruct Hix as [(?&?&?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup|
-                     [j Hj]%elem_of_map_to_list%elem_of_list_lookup_1].
+                     [j Hj]%elem_of_map_to_list%list_elem_of_lookup_1].
     + simplify_eq/=. rewrite !Z2Nat.id in Hlt; eauto with lia.
     + apply map_Forall_to_list in Hσ.
       by eapply Forall_lookup in Hσ; eauto; simpl in *.
@@ -201,9 +201,9 @@ Proof.
     end. by case (vs !! _); simplify_option_eq.
   - destruct (decide _) as [[??]|[<-%dec_stable|[<-%dec_stable ?]]%not_and_l_alt].
     + rewrite !binder_delete_insert // !binder_delete_delete; eauto with f_equal.
-    + by rewrite /= delete_insert_delete delete_idemp.
-    + by rewrite /= binder_delete_insert // delete_insert_delete
-        !binder_delete_delete delete_idemp.
+    + by rewrite /= delete_insert_eq delete_delete_eq.
+    + by rewrite /= binder_delete_insert // delete_insert_eq
+        !binder_delete_delete delete_delete_eq.
 Qed.
 Lemma subst_map_singleton x v e :
   subst_map {[x:=v]} e = subst x v e.
@@ -223,7 +223,7 @@ Lemma subst_map_binder_insert_2 b1 v1 b2 v2 vs e :
 Proof.
   destruct b1 as [|s1], b2 as [|s2]=> /=; auto using subst_map_insert.
   rewrite subst_map_insert. destruct (decide (s1 = s2)) as [->|].
-  - by rewrite delete_idemp subst_subst delete_insert_delete.
+  - by rewrite delete_delete_eq subst_subst delete_insert_eq.
   - by rewrite delete_insert_ne // subst_map_insert subst_subst_ne.
 Qed.
 Lemma subst_map_binder_insert_2_empty b1 v1 b2 v2 e :
diff --git a/theories/examples/input_lang/interp.v b/theories/examples/input_lang/interp.v
index 7be0c30..0301c9a 100644
--- a/theories/examples/input_lang/interp.v
+++ b/theories/examples/input_lang/interp.v
@@ -182,7 +182,7 @@ Section interp.
   Global Instance ArrEquiv {A B : Set} : Equiv (A [→] B) :=
     fun f g => ∀ x, f x = g x.
 
-  Global Instance ArrDist {A B : Set} `{Dist B} : Dist (A [→] B) :=
+  Global Instance ArrDist {A B : Set} `{!Dist B} : Dist (A [→] B) :=
     fun n => fun f g => ∀ x, f x ≡{n}≡ g x.
 
   Global Instance ren_scope_proper {S S'} :
@@ -216,7 +216,7 @@ Section interp.
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_ren.
-        apply bi.siProp.internal_eq_soundness.
+        apply (@bi.internal_eq.internal_eq_soundness siProp _).
         iLöb as "IH".
         rewrite {2}interp_rec_unfold.
         rewrite {2}(interp_rec_unfold (interp_expr e)).
@@ -285,7 +285,7 @@ Section interp.
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_subst.
-        apply bi.siProp.internal_eq_soundness.
+        apply (@bi.internal_eq.internal_eq_soundness siProp _).
         iLöb as "IH".
         rewrite {2}interp_rec_unfold.
         rewrite {2}(interp_rec_unfold (interp_expr e)).
diff --git a/theories/examples/input_lang/logrel.v b/theories/examples/input_lang/logrel.v
index 245e18d..e0f8962 100644
--- a/theories/examples/input_lang/logrel.v
+++ b/theories/examples/input_lang/logrel.v
@@ -459,7 +459,7 @@ Proof.
     iExists l. iModIntro. iSplit; eauto.
     iExists l. iSplit; eauto.
   - iIntros "Hst HΦ Hstuck".
-    iAssert ((IT_to_V (Ret n)) ≡ Some (RetV n))%I as "HEQ".
+    iAssert ((IT_to_V (Ret n : IT (gReifiers_ops rs) natO)) ≡ Some (RetV n))%I as "HEQ".
     { by rewrite IT_to_V_Ret. }
     iDestruct (internal_eq_rewrite _ _
                  (λ x, from_option Φ True%I x)
diff --git a/theories/examples/input_lang_callcc/interp.v b/theories/examples/input_lang_callcc/interp.v
index ffaae97..2b5da77 100644
--- a/theories/examples/input_lang_callcc/interp.v
+++ b/theories/examples/input_lang_callcc/interp.v
@@ -292,7 +292,7 @@ Section interp.
   Global Instance ArrEquiv {A B : Set} : Equiv (A [→] B) :=
     fun f g => ∀ x, f x = g x.
 
-  Global Instance ArrDist {A B : Set} `{Dist B} : Dist (A [→] B) :=
+  Global Instance ArrDist {A B : Set} `{!Dist B} : Dist (A [→] B) :=
     fun n => fun f g => ∀ x, f x ≡{n}≡ g x.
 
   Global Instance ren_scope_proper {S S'} :
@@ -338,7 +338,7 @@ Section interp.
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_ren.
-        apply bi.siProp.internal_eq_soundness.
+        apply (@bi.internal_eq.internal_eq_soundness siProp _).
         iLöb as "IH".
         rewrite {2}interp_rec_unfold.
         rewrite {2}(interp_rec_unfold (interp_expr e)).
@@ -432,7 +432,7 @@ Section interp.
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_subst.
-        apply bi.siProp.internal_eq_soundness.
+        apply (@bi.internal_eq.internal_eq_soundness siProp _).
         iLöb as "IH".
         rewrite {2}interp_rec_unfold.
         rewrite {2}(interp_rec_unfold (interp_expr e)).
@@ -910,8 +910,7 @@ Section interp.
           * repeat f_equiv. unfold s1.
             setoid_rewrite ofe_iso_12.
             symmetry. by apply gState_recomp_decomp.
-          * intro; simpl.
-            f_equiv. done.
+          * intros ?; simpl; done.
       - repeat f_equiv.
         unfold s1.
         setoid_rewrite ofe_iso_12.
diff --git a/theories/examples/input_lang_callcc/logrel.v b/theories/examples/input_lang_callcc/logrel.v
index 33b5ea8..a5d9b06 100644
--- a/theories/examples/input_lang_callcc/logrel.v
+++ b/theories/examples/input_lang_callcc/logrel.v
@@ -823,7 +823,7 @@ Proof.
     iExists l. iModIntro. iSplit; eauto.
     iExists l. iSplit; eauto.
   - iIntros "Hst HΦ Hstuck".
-    iAssert ((IT_to_V (Ret n)) ≡ Some (RetV n))%I as "HEQ".
+    iAssert ((IT_to_V (Ret n : IT (gReifiers_ops rs) natO)) ≡ Some (RetV n))%I as "HEQ".
     { by rewrite IT_to_V_Ret. }
     iDestruct (internal_eq_rewrite _ _
                  (λ x, from_option Φ True%I x)
diff --git a/theories/examples/lang_callcc/interp.v b/theories/examples/lang_callcc/interp.v
index ec769c8..3fd8ded 100644
--- a/theories/examples/lang_callcc/interp.v
+++ b/theories/examples/lang_callcc/interp.v
@@ -232,7 +232,7 @@ Section interp.
   Global Instance ArrEquiv {A B : Set} : Equiv (A [→] B) :=
     fun f g => ∀ x, f x = g x.
 
-  Global Instance ArrDist {A B : Set} `{Dist B} : Dist (A [→] B) :=
+  Global Instance ArrDist {A B : Set} `{!Dist B} : Dist (A [→] B) :=
     fun n => fun f g => ∀ x, f x ≡{n}≡ g x.
 
   Global Instance ren_scope_proper {S S'} :
@@ -276,7 +276,7 @@ Section interp.
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_ren.
-        apply bi.siProp.internal_eq_soundness.
+        apply (@bi.internal_eq.internal_eq_soundness siProp _).
         iLöb as "IH".
         rewrite {2}interp_rec_unfold.
         rewrite {2}(interp_rec_unfold (interp_expr e)).
@@ -367,7 +367,7 @@ Section interp.
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_subst.
-        apply bi.siProp.internal_eq_soundness.
+        apply (@bi.internal_eq.internal_eq_soundness siProp _).
         iLöb as "IH".
         rewrite {2}interp_rec_unfold.
         rewrite {2}(interp_rec_unfold (interp_expr e)).
diff --git a/theories/examples/lang_callcc/logrel.v b/theories/examples/lang_callcc/logrel.v
index 5822eda..3e984ad 100644
--- a/theories/examples/lang_callcc/logrel.v
+++ b/theories/examples/lang_callcc/logrel.v
@@ -749,7 +749,7 @@ Proof.
     iExists l. iModIntro. iSplit; eauto.
     iExists l. iSplit; eauto.
   - iIntros "Hs HΦ Hstuck".
-    iAssert ((IT_to_V (Ret n)) ≡ Some (RetV n))%I as "HEQ".
+    iAssert ((IT_to_V (Ret n : IT (gReifiers_ops rs) natO)) ≡ Some (RetV n))%I as "HEQ".
     { by rewrite IT_to_V_Ret. }
     iDestruct (internal_eq_rewrite _ _
                  (λ x, from_option Φ True%I x)
diff --git a/theories/gitree.v b/theories/gitree.v
index 19f40f5..ad1e7e1 100644
--- a/theories/gitree.v
+++ b/theories/gitree.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Export base tactics classes.
+From iris.proofmode Require Export base proofmode classes.
 From iris.base_logic.lib Require Export own fancy_updates invariants.
 From gitrees Require Export prelude.
 From gitrees.gitree Require Export core subofe reify greifiers reductions weakestpre lambda.
diff --git a/theories/gitree/core.v b/theories/gitree/core.v
index 8cec986..ad3a4a5 100644
--- a/theories/gitree/core.v
+++ b/theories/gitree/core.v
@@ -1,6 +1,6 @@
 From iris.prelude Require Import options.
 From iris.algebra Require cofe_solver.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Export base_logic.
 From gitrees Require Import prelude.
 
@@ -51,9 +51,9 @@ Notation "@[ Σ1 ; .. ; Σn ]" :=
 
 Class subEff (F E : opsInterp) := {
     subEff_opid : opid F → opid E;
-    subEff_ins {op: opid F} {X} `{Cofe X} :
+    subEff_ins {op: opid F} {X} `{!Cofe X} :
       Ins (F op) ♯ X ≃ Ins (E (subEff_opid op)) ♯ X;
-    subEff_outs {op: opid F} {X} `{Cofe X} :
+    subEff_outs {op: opid F} {X} `{!Cofe X} :
       Outs (F op) ♯ X ≃ Outs (E (subEff_opid op)) ♯ X;
   }.
 Definition subEff_id F : subEff F F :=
@@ -208,7 +208,7 @@ Section smart.
   Proof. apply (fixpoint_unfold pre_Bottom). Qed.
 
   (** Injectivity of the constructors *)
-  Lemma Tau_inj' (α β : laterO IT) {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma Tau_inj' (α β : laterO IT) {PROP : bi} `{!Sbi PROP} :
     (α ≡ β ⊣⊢ (Tau α ≡ Tau β : PROP))%I.
   Proof.
     iSplit.
@@ -222,7 +222,7 @@ Section smart.
       iPoseProof (sum_equivI with "H") as "H".
       done.
   Qed.
-  Lemma Ret_inj' (k m : A) {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma Ret_inj' (k m : A) {PROP : bi} `{!Sbi PROP} :
     (k ≡ m ⊣⊢ (Ret k ≡ Ret m : PROP))%I.
   Proof.
     iSplit.
@@ -234,7 +234,7 @@ Section smart.
       repeat iPoseProof (sum_equivI with "H") as "H".
       done.
   Qed.
-  Lemma Err_inj' (e e' : error) {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma Err_inj' (e e' : error) {PROP : bi} `{!Sbi PROP} :
     (e ≡ e' ⊣⊢ (Err e ≡ Err e' : PROP))%I.
   Proof.
     iSplit.
@@ -246,7 +246,7 @@ Section smart.
       repeat iPoseProof (sum_equivI with "H") as "H".
       done.
   Qed.
-  Lemma Fun_inj' (f g : laterO (IT -n> IT)) {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma Fun_inj' (f g : laterO (IT -n> IT)) {PROP : bi} `{!Sbi PROP} :
     (f ≡ g ⊣⊢ (Fun f ≡ Fun g : PROP))%I.
   Proof.
     iSplit.
@@ -259,7 +259,7 @@ Section smart.
       done.
   Qed.
 
-  Lemma Vis_inj_op' op1 op2 i1 i2 k1 k2 {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma Vis_inj_op' op1 op2 i1 i2 k1 k2 {PROP : bi} `{!Sbi PROP} :
     (Vis op1 i1 k1 ≡ Vis op2 i2 k2 ⊢ ⌜op1 = op2⌝ : PROP)%I.
   Proof.
     iIntros "H".
@@ -272,7 +272,7 @@ Section smart.
     done.
   Qed.
 
-  Lemma Vis_inj' op i1 i2 k1 k2  {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma Vis_inj' op i1 i2 k1 k2  {PROP : bi} `{!Sbi PROP} :
     (Vis op i1 k1 ≡ Vis op i2 k2 ⊢ i1 ≡ i2 ∧ k1 ≡ k2 : PROP)%I.
   Proof.
     iIntros "H".
@@ -287,7 +287,7 @@ Section smart.
     simpl. iPoseProof (prod_equivI with "H") as "[$ $]".
   Qed.
 
-  Lemma IT_ret_tau_ne k α {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_ret_tau_ne k α {PROP : bi} `{!Sbi PROP} :
     (Ret k ≡ Tau α ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
@@ -298,7 +298,7 @@ Section smart.
     iPoseProof (sum_equivI with "H") as "H".
     done.
   Qed.
-  Lemma IT_fun_tau_ne f α {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_fun_tau_ne f α {PROP : bi} `{!Sbi PROP} :
     (Fun f ≡ Tau α ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
@@ -308,7 +308,7 @@ Section smart.
     iPoseProof (sum_equivI with "H2") as "H2".
     by iPoseProof (sum_equivI with "H2") as "H2".
   Qed.
-  Lemma IT_ret_vis_ne n op i k {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_ret_vis_ne n op i k {PROP : bi} `{!Sbi PROP} :
     (Ret n ≡ Vis op i k ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
@@ -318,7 +318,7 @@ Section smart.
     iPoseProof (sum_equivI with "H2") as "H".
     done.
   Qed.
-  Lemma IT_fun_vis_ne f op i ko {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_fun_vis_ne f op i ko {PROP : bi} `{!Sbi PROP} :
     (Fun f ≡ Vis op i ko ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
@@ -327,7 +327,7 @@ Section smart.
     rewrite !IT_unfold_fold. simpl.
     by iPoseProof (sum_equivI with "H2") as "H2".
   Qed.
-  Lemma IT_tau_vis_ne α op i k {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_tau_vis_ne α op i k {PROP : bi} `{!Sbi PROP} :
     (Tau α ≡ Vis op i k ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
@@ -337,7 +337,7 @@ Section smart.
     iPoseProof (sum_equivI with "H2") as "H2".
     done.
   Qed.
-  Lemma IT_ret_fun_ne k f {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_ret_fun_ne k f {PROP : bi} `{!Sbi PROP} :
     (Ret k ≡ Fun f ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
@@ -346,7 +346,7 @@ Section smart.
     rewrite !IT_unfold_fold. simpl.
     by repeat iPoseProof (sum_equivI with "H2") as "H2".
   Qed.
-  Lemma IT_tau_err_ne α e {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_tau_err_ne α e {PROP : bi} `{!Sbi PROP} :
     (Tau α ≡ Err e ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
@@ -355,7 +355,7 @@ Section smart.
     rewrite !IT_unfold_fold /=.
     by repeat iPoseProof (sum_equivI with "H2") as "H2".
   Qed.
-  Lemma IT_ret_err_ne n e {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_ret_err_ne n e {PROP : bi} `{!Sbi PROP} :
     (Ret n ≡ Err e ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
@@ -364,7 +364,7 @@ Section smart.
     rewrite !IT_unfold_fold /=.
     by repeat iPoseProof (sum_equivI with "H2") as "H2".
   Qed.
-  Lemma IT_fun_err_ne n e {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_fun_err_ne n e {PROP : bi} `{!Sbi PROP} :
     (Fun n ≡ Err e ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
@@ -373,7 +373,7 @@ Section smart.
     rewrite !IT_unfold_fold /=.
     by repeat iPoseProof (sum_equivI with "H2") as "H2".
   Qed.
-  Lemma IT_vis_err_ne op i k e {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_vis_err_ne op i k e {PROP : bi} `{!Sbi PROP} :
     (Vis op i k ≡ Err e ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
@@ -729,8 +729,7 @@ Section ticks.
     { by rewrite H1. }
     revert H2. rewrite /Tick /=.
     rewrite !IT_unfold_fold. intros H2.
-    apply (Next_inj (S k) x y); last lia.
-    by eapply inr_ne_inj, inl_ne_inj.
+    by apply dist_later_S, (inj Next), (inj inr), (inj inl).
   Qed.
   Global Instance Tick_contractive : Contractive Tick.
   Proof. solve_contractive. Qed.
@@ -756,20 +755,20 @@ Section ticks.
     cbn[plus]. by rewrite !Tick_n_S IHk.
   Qed.
 
-  Lemma IT_ret_tick_ne k α {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_ret_tick_ne k α {PROP : bi} `{!Sbi PROP} :
     (Ret k ≡ Tick α ⊢ False : PROP)%I.
   Proof. apply IT_ret_tau_ne. Qed.
-  Lemma IT_fun_tick_ne f α {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_fun_tick_ne f α {PROP : bi} `{!Sbi PROP} :
     (Fun f ≡ Tick α ⊢ False : PROP)%I.
   Proof. apply IT_fun_tau_ne. Qed.
-  Lemma IT_tick_vis_ne α op i k {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_tick_vis_ne α op i k {PROP : bi} `{!Sbi PROP} :
     (Tick α ≡ Vis op i k ⊢ False : PROP)%I.
   Proof. apply IT_tau_vis_ne. Qed.
-  Lemma IT_tick_err_ne α e {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_tick_err_ne α e {PROP : bi} `{!Sbi PROP} :
     (Tick α ≡ Err e ⊢ False : PROP)%I.
   Proof. apply IT_tau_err_ne. Qed.
 
-  #[export] Instance from_modal_tick x y      {PROP : bi} `{!BiInternalEq PROP} :
+  #[export] Instance from_modal_tick x y      {PROP : bi} `{!Sbi PROP} :
     FromModal (PROP1:=PROP) (PROP2:=PROP) True (modality_instances.modality_laterN 1)
               (▷ (x ≡ y) : PROP)%I (Tick x ≡ Tick y) (x ≡ y).
   Proof.
@@ -778,7 +777,7 @@ Section ticks.
   Qed.
 
   #[export] Instance into_laterN_tick only_head n n' (α β : IT)
-    {PROP : bi} `{!BiInternalEq PROP} :
+    {PROP : bi} `{!Sbi PROP} :
     nat_cancel.NatCancel n 1 n' 0 →
     IntoLaterN (PROP:=PROP) only_head n (Tick α ≡ Tick β) (α ≡ β) | 2.
   Proof.
@@ -809,7 +808,7 @@ Section ticks.
     - right. right. right. right. exists op,i,k. done.
   Qed.
 
-  Lemma IT_dont_confuse' (α : IT) {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_dont_confuse' (α : IT) {PROP : bi} `{!Sbi PROP} :
     (⊢ (∃ e,      α ≡ Err e)
      ∨ (∃ n,      α ≡ Ret n)
      ∨ (∃ f,      α ≡ Fun f)
@@ -859,7 +858,7 @@ Section ITV.
                   | FunV f, FunV g => dist n f g
                   | _, _ => False
                   end.
-  #[export] Instance ITV_dist_equiv n : Equivalence (@dist ITV _ n).
+  #[export] Instance ITV_dist_equiv n : Equivalence (@dist _ ITV _ n).
   Proof.
     unfold dist.
     split.
@@ -895,15 +894,15 @@ Section ITV.
     + split; first tauto.
       intros H. apply (H 0).
   Qed.
-  Lemma ITV_dist_lt n m (x y : ITV) :
-    x ≡{n}≡ y → m < n → x ≡{m}≡ y.
+  Lemma ITV_dist_le n m (x y : ITV) :
+    x ≡{n}≡ y → m ≤ n → x ≡{m}≡ y.
   Proof.
     unfold dist.
-    destruct x as [n1|f1], y as [n2|f2]; simpl; eauto using dist_lt.
+    destruct x as [n1|f1], y as [n2|f2]; simpl; eauto using dist_le.
   Qed.
 
   Canonical Structure ITVO := Ofe ITV ({| mixin_equiv_dist := ITV_equiv_dist;
-                                mixin_dist_lt := ITV_dist_lt;
+                                mixin_dist_le := ITV_dist_le;
                                 mixin_dist_equivalence := ITV_dist_equiv
                                        |}).
 
@@ -1023,7 +1022,7 @@ Section ITV.
     - apply IT_to_V_Fun.
   Qed.
 
-  Lemma IT_of_to_V α v {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_of_to_V α v {PROP : bi} `{!Sbi PROP} :
     (IT_to_V α ≡ Some v ⊢ IT_of_V v ≡ α : PROP).
   Proof.
     iIntros "H".
@@ -1069,7 +1068,7 @@ Section ITV.
       rewrite option_equiv_Forall2. inversion 1.
   Qed.
 
-  Lemma IT_to_V_None α {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_to_V_None α {PROP : bi} `{!Sbi PROP} :
     (IT_to_V α ≡ None ⊢ (∃ e, α ≡ Err e)
                      ∨ (∃ β, α ≡ Tick β)
                      ∨ (∃ op i k, α ≡ Vis op i k)
@@ -1088,7 +1087,7 @@ Section ITV.
       done.
   Qed.
 
-  Lemma IT_of_V_inj' αv βv {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_of_V_inj' αv βv {PROP : bi} `{!Sbi PROP} :
     (IT_of_V αv ≡ IT_of_V βv ⊢ αv ≡ βv : PROP)%I.
   Proof.
     iIntros "H".
@@ -1096,8 +1095,8 @@ Section ITV.
     - iPoseProof (Ret_inj' with"H") as"H".
       by iRewrite "H". (*XXX: easier proof?*)
     - iExFalso. iApply (IT_ret_fun_ne with "H").
-    - iExFalso. iApply (IT_ret_fun_ne). iApply internal_eq_sym.
-      iExact "H".
+    - iExFalso. iDestruct (internal_eq_sym with "H") as "H".
+      iApply (IT_ret_fun_ne with "H").
     - iPoseProof (Fun_inj' with "H") as "H".
       by iRewrite "H".
   Qed.
diff --git a/theories/gitree/greifiers.v b/theories/gitree/greifiers.v
index d36c978..e53918e 100644
--- a/theories/gitree/greifiers.v
+++ b/theories/gitree/greifiers.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import list.
-From iris.proofmode Require Import classes tactics.
+From iris.proofmode Require Import classes proofmode.
 From iris.base_logic.lib Require Export invariants.
 From gitrees Require Import prelude.
 From gitrees.gitree Require Import core reify.
@@ -42,17 +42,6 @@ Section greifiers_generic.
     {| opid := { i : fin n & opid (sReifier_ops (rs !!! i)) };
       opsInterp_lookup := λ iop, sReifier_ops (rs !!! projT1 iop) (projT2 iop)
     |}.
-  Next Obligation.
-    intros n rs.
-    unfold EqDecision. intros [i1 x1] [i2 x2].
-    unfold Decision.
-    destruct (decide (i1 = i2)) as [<-|Hi].
-    - destruct (decide (x1 = x2)) as [<-|Hx].
-      + left. reflexivity.
-      + right. naive_solver.
-    - right. naive_solver.
-  Qed.
-
   Fixpoint gReifiers_state {n} (rs : gReifiers n) : oFunctor :=
     match rs with
     | gReifiers_nil => unitO
@@ -481,7 +470,7 @@ Section greifiers.
     (gReifiers_re CtxDep rs op (i, σ, k) ≡ Some (o,σ',th)
      ⊢@{iProp} reify (sr CtxDep rs) (Vis op i k : IT _ A) σ ≡ (σ', Tau $ o, listO_map Tau th))%I.
   Proof.
-    apply uPred.internal_eq_entails=>m.
+    apply internal_eq_entails=>m.
     intros H. apply reify_vis_dist_ctx_dep. exact H.
   Qed.
 
@@ -490,7 +479,7 @@ Section greifiers.
     (gReifiers_re NotCtxDep rs op (i, σ) ≡ Some (o,σ',th)
      ⊢@{iProp} reify (sr NotCtxDep rs) (Vis op i k : IT _ A) σ ≡ (σ', Tau $ k o, listO_map Tau th))%I.
   Proof.
-    apply uPred.internal_eq_entails=>m.
+    apply internal_eq_entails=>m.
     intros H. apply reify_vis_dist_ctx_indep. exact H.
   Qed.
 
@@ -506,7 +495,7 @@ Section greifiers.
        (subEff_ins x, sR_state s1, k ◎ (subEff_outs ^-1)) ≡
        Some (y, sR_state s2, th).
   Proof.
-    apply uPred.internal_eq_entails=>m.
+    apply internal_eq_entails=>m.
     intros H'.
     rewrite (@sR_re _ CtxDep); last first.
     - rewrite H'.
@@ -525,7 +514,7 @@ Section greifiers.
        (subEff_ins x, sR_state s1) ≡
        Some (subEff_outs y, sR_state s2, th).
   Proof.
-    apply uPred.internal_eq_entails=>m.
+    apply internal_eq_entails=>m.
     apply (@sR_re _ NotCtxDep).
   Qed.
 
@@ -541,7 +530,7 @@ Section greifiers.
        (subEff_ins x, gState_recomp CtxDep rest (sR_state σ), k ◎ (subEff_outs ^-1))
        ≡ Some (y, gState_recomp CtxDep rest (sR_state σ'), th).
   Proof.
-    apply uPred.internal_eq_entails=>m.
+    apply internal_eq_entails=>m.
     intros He.
     eapply (@sR_re _ CtxDep) in He.
     rewrite (gReifiers_re_idx CtxDep)//.
@@ -560,7 +549,7 @@ Section greifiers.
        (subEff_ins x, gState_recomp NotCtxDep rest (sR_state σ))
        ≡ Some (subEff_outs y, gState_recomp NotCtxDep rest (sR_state σ'), th).
   Proof.
-    apply uPred.internal_eq_entails=>m.
+    apply internal_eq_entails=>m.
     intros He.
     eapply (@sR_re _ NotCtxDep) in He.
     pose proof (@gReifiers_re_idx sz NotCtxDep sR_idx rs X _ (subEff_opid op)
diff --git a/theories/gitree/reductions.v b/theories/gitree/reductions.v
index 3ce4762..5117717 100644
--- a/theories/gitree/reductions.v
+++ b/theories/gitree/reductions.v
@@ -1,7 +1,7 @@
-From iris.proofmode Require Import classes tactics.
+From iris.proofmode Require Import classes proofmode.
 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Import list.
-From iris.bi.lib Require Import fixpoint.
+From iris.bi.lib Require Import fixpoint_mono.
 From gitrees Require Import prelude.
 From gitrees.gitree Require Import core reify.
 
@@ -545,24 +545,24 @@ Section internal_step.
     intros Hprf.
     destruct (IT_dont_confuse α)
       as [[e Ha] | [[n Ha] | [ [g Ha] | [[α' Ha]|[op [i [k Ha]]]] ]]].
-    + exfalso. eapply uPred.pure_soundness.
+    + exfalso. eapply (sbi.pure_soundness (PROP:=iProp)).
       iPoseProof (Hprf) as "H".
       iDestruct "H" as (β σ') "[Ha Hs]". rewrite Ha.
-      iApply (IT_tick_err_ne). iApply internal_eq_sym.
-      by iApply "Ha".
-    + exfalso. eapply uPred.pure_soundness.
+      iDestruct (internal_eq_sym with "Ha") as "Hsym".
+      by iApply (IT_tick_err_ne with "Hsym").
+    + exfalso. eapply (sbi.pure_soundness (PROP:=iProp)).
       iPoseProof (Hprf) as "H".
       iDestruct "H" as (β σ') "[Ha Hs]". rewrite Ha.
       iApply (IT_ret_tick_ne with "Ha").
-    + exfalso. eapply uPred.pure_soundness.
+    + exfalso. eapply (sbi.pure_soundness (PROP:=iProp)).
       iPoseProof (Hprf) as "H".
       iDestruct "H" as (β σ') "[Ha Hs]". rewrite Ha.
       iApply (IT_fun_tick_ne with "Ha").
     + exists α',σ. by econstructor; eauto.
-    + exfalso. eapply uPred.pure_soundness.
+    + exfalso. eapply (sbi.pure_soundness (PROP:=iProp)).
       iPoseProof (Hprf) as "H".
       iDestruct "H" as (β σ') "[Ha Hs]". rewrite Ha.
-      iApply (IT_tick_vis_ne). by iApply (internal_eq_sym with "Ha").
+      iDestruct (internal_eq_sym with "Ha") as "Hsym". by iApply (IT_tick_vis_ne with "Hsym").
   Qed.
 
   (* ctx-free steps *)
@@ -573,20 +573,20 @@ Section internal_step.
     intros Hprf.
     destruct (IT_dont_confuse α)
       as [[e Ha] | [[n Ha] | [ [g Ha] | [[α' Ha]|[op [i [k Ha]]]] ]]].
-    + exfalso. eapply uPred.pure_soundness.
+    + exfalso. eapply (sbi.pure_soundness (PROP:=iProp)).
       iPoseProof (Hprf) as "H".
       iDestruct "H" as (β σ' en op i k) "[Ha _]". rewrite Ha.
-      iApply (IT_vis_err_ne). iApply internal_eq_sym.
-      by iApply "Ha".
-    + exfalso. eapply uPred.pure_soundness.
+      iDestruct (internal_eq_sym with "Ha") as "Hsym".
+      by iApply (IT_vis_err_ne with "Hsym").
+    + exfalso. eapply (sbi.pure_soundness (PROP:=iProp)).
       iPoseProof (Hprf) as "H".
       iDestruct "H" as (β σ' en op i k) "[Ha _]". rewrite Ha.
       iApply (IT_ret_vis_ne with "Ha").
-    + exfalso. eapply uPred.pure_soundness.
+    + exfalso. eapply (sbi.pure_soundness (PROP:=iProp)).
       iPoseProof (Hprf) as "H".
       iDestruct "H" as (β σ' en op i k) "[Ha _]". rewrite Ha.
       iApply (IT_fun_vis_ne with "Ha").
-    + exfalso. eapply uPred.pure_soundness.
+    + exfalso. eapply (sbi.pure_soundness (PROP:=iProp)).
       iPoseProof (Hprf) as "H".
       iDestruct "H" as (β σ' en op i k) "[Ha _]". rewrite Ha.
       iApply (IT_tick_vis_ne with "Ha").
@@ -597,7 +597,7 @@ Section internal_step.
       }
       * exists α',σ1, en. eapply external_step_reify; eauto.
         rewrite -Ha' -Hr; repeat f_equiv; eauto.
-      * exfalso. eapply uPred.pure_soundness.
+      * exfalso. eapply (sbi.pure_soundness (PROP:=iProp)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (β σ' en' op' i' k') "[_ Hb]".
         assert (reify r (Vis op i k) σ ≡ reify r α σ) as Har.
@@ -607,7 +607,7 @@ Section internal_step.
         iPoseProof (prod_equivI with "Hb") as "[Hb'' Hb']".
         iPoseProof (prod_equivI with "Hb''") as "[_ Hb'''']".
         simpl. rewrite Ha'.
-        iApply (IT_tick_err_ne). iApply (internal_eq_sym with "Hb''''").
+        iDestruct (internal_eq_sym with "Hb''''") as "Hsym". by iApply (IT_tick_err_ne with "Hsym").
   Qed.
 
   Local Lemma internal_step_safe_disj α σ :
@@ -645,8 +645,8 @@ Section internal_step.
     iInduction n as [| n IH] "G" forall (α e2 σ l).
     - rewrite internal_steps_0.
       iDestruct "H" as "(H1 & H2 & H3)".
-      iRewrite "H1"; iRewrite "H2"; iRewrite "H3".
       rewrite tp_internal_steps_0.
+      iRewrite "H1"; iRewrite "H2"; iRewrite "H3".
       by rewrite app_nil_r.
     - rewrite internal_steps_S.
       iDestruct "H" as "(%γ & %σ'' & %t & %t' & G1 & G2 & G3)".
@@ -656,7 +656,11 @@ Section internal_step.
       + by iApply internal_step_tp_internal_step.
       + iSpecialize ("G" $! γ (e2 ++ t) σ'' t').
         rewrite -app_assoc.
-        iRewrite - "G1" in "G".
+        iSymmetry in "G1".
+        iApply (internal_eq_rewrite (PROP := iProp) (t ++ t') l
+                  (λ l0, tp_internal_steps (e1 ++ γ :: e2 ++ t) σ''
+                    (e1 ++ β :: e2 ++ l0) σ' n)%I with "G1").
+        { solve_proper. }
         by iApply "G".
   Qed.
 
@@ -690,10 +694,11 @@ Section internal_step.
   Lemma internal_step_err σ e β σ' en : internal_step (Err e) σ β σ' en ⊢ False.
   Proof.
     rewrite /internal_step/=. iDestruct 1 as "[[H _]|H]".
-    - iApply (IT_tick_err_ne).
-      by iApply (internal_eq_sym with "H").
-    - iDestruct "H" as (op i k) "[H _]". iApply (IT_vis_err_ne).
-      by iApply internal_eq_sym.
+    - iDestruct (internal_eq_sym with "H") as "Hsym".
+      by iApply (IT_tick_err_ne with "Hsym").
+    - iDestruct "H" as (op i k) "[H _]".
+      iDestruct (internal_eq_sym with "H") as "Hsym".
+      by iApply (IT_vis_err_ne with "Hsym").
   Qed.
 
   Lemma internal_step_tick α β σ σ' en :
@@ -709,8 +714,8 @@ Section internal_step.
     internal_step (Vis op i ko) σ β σ' en ⊢ reify r (Vis op i ko) σ ≡ (σ', Tick β, en).
   Proof.
     simpl. iDestruct 1 as "[[H1 H2]|H]".
-    - iExFalso. iApply IT_tick_vis_ne.
-      by iApply internal_eq_sym.
+    - iExFalso. iDestruct (internal_eq_sym with "H1") as "Hsym".
+      by iApply (IT_tick_vis_ne with "Hsym").
     - iDestruct "H" as (op' i' ko') "[H1 $]".
   Qed.
 
@@ -739,17 +744,26 @@ Section internal_step.
     rewrite internal_steps_unfold.
     iDestruct 1 as "[[Hk [Ht Hs]] | H]".
     - iExFalso. destruct βv; iSimpl in "Ht".
-      ++ iApply (IT_ret_tick_ne).
-         iApply (internal_eq_sym with "Ht").
-      ++ iApply (IT_fun_tick_ne).
-         by iApply (internal_eq_sym with "Ht").
+      ++ iSymmetry in "Ht".
+         by iApply (IT_ret_tick_ne with "Ht").
+      ++ iSymmetry in "Ht".
+         by iApply (IT_fun_tick_ne with "Ht").
     - iDestruct "H" as (k' α1 σ1 l' l'') "[Hl [% [Hs Hss]]]".
       iExists k'. iSplit; first by eauto.
       rewrite internal_step_tick.
       iDestruct "Hs" as "[Ha [Hs1 Hs2]]". iNext.
-      iRewrite -"Ha". iRewrite "Hs1".
-      iRewrite "Hl".
-      iRewrite "Hs2".
+      iApply (internal_eq_rewrite (PROP := iProp) α1 α
+                (λ α0, internal_steps α0 σ (IT_of_V βv) σ' l k')%I with "Ha").
+      { solve_proper. }
+      iSymmetry in "Hs1".
+      iApply (internal_eq_rewrite (PROP := iProp) σ1 σ
+                (λ σ0, internal_steps α1 σ0 (IT_of_V βv) σ' l k')%I with "Hs1").
+      { solve_proper. }
+      iRewrite "Hs2" in "Hl". iSimpl in "Hl".
+      iSymmetry in "Hl".
+      iApply (internal_eq_rewrite (PROP := iProp) l'' l
+                (λ l0, internal_steps α1 σ1 (IT_of_V βv) σ' l0 k')%I with "Hl").
+      { solve_proper. }
       done.
   Qed.
 
@@ -812,8 +826,8 @@ Section internal_step_ctx_indep.
       iRewrite "Hf" in "H".
       rewrite {1}/internal_step. iSimpl in "H".
       iDestruct "H" as "[[H _]|H]".
-      + iExFalso. iApply (IT_tick_vis_ne).
-        iApply internal_eq_sym. done.
+      + iExFalso. iDestruct (internal_eq_sym with "H") as "Hsym".
+        by iApply (IT_tick_vis_ne with "Hsym").
       + iDestruct "H" as (op' i' k') "[#Ha Hr]".
         iPoseProof (Vis_inj_op' with "Ha") as "<-".
         iPoseProof (Vis_inj' with "Ha") as "[Hi Hk]".
diff --git a/theories/gitree/reify.v b/theories/gitree/reify.v
index 427800a..6456674 100644
--- a/theories/gitree/reify.v
+++ b/theories/gitree/reify.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import list.
-From iris.proofmode Require Import classes tactics.
+From iris.proofmode Require Import classes proofmode.
 From gitrees Require Import prelude.
 From gitrees.gitree Require Import core.
 
@@ -518,7 +518,7 @@ Section reify_props.
   Qed.
 
   Lemma reify_vis_cont r op i k1 k2 σ1 σ2 β th
-    {PROP : bi} `{!BiInternalEq PROP} :
+    {PROP : bi} `{!Sbi PROP} :
     (reify (a := NotCtxDep) (A := A) (r := r) (Vis op i k1) σ1 ≡ (σ2, Tick β, th) ⊢
      reify (Vis op i (laterO_map k2 ◎ k1)) σ1 ≡ (σ2, Tick (k2 β), th) : PROP)%I.
   Proof.
@@ -528,7 +528,8 @@ Section reify_props.
       iPoseProof (prod_equivI with "Hr") as "(Ht & _)".
       simpl.
       iPoseProof (prod_equivI with "Ht") as "(_ & Hk)".
-      iApply (IT_tick_err_ne). by iApply internal_eq_sym.
+      iDestruct (internal_eq_sym with "Hk") as "Hk".
+      by iApply (IT_tick_err_ne with "Hk").
     - rewrite reify_vis_eq_ctx_indep; last first.
       { by rewrite Hre. }
       rewrite reify_vis_eq_ctx_indep; last first.
@@ -548,7 +549,7 @@ Section reify_props.
 
   Lemma reify_input_cont_inv r op i (k1 : _ -n> laterO (IT NotCtxDep r))
     (k2 : IT _ r -n> IT _ r) σ1 σ2 β th
-    {PROP : bi} `{!BiInternalEq PROP} :
+    {PROP : bi} `{!Sbi PROP} :
     (reify (Vis op i (laterO_map k2 ◎ k1)) σ1 ≡ (σ2, Tick β, th)
      ⊢ ∃ α, reify (Vis op i k1) σ1 ≡ (σ2, Tick α, th) ∧ ▷ (β ≡ k2 α)
          : PROP)%I.
@@ -558,7 +559,8 @@ Section reify_props.
       iIntros "Hr". iExFalso.
       iPoseProof (prod_equivI with "Hr") as "[Hr Hk]".
       iPoseProof (prod_equivI with "Hr") as "[Hr Hs]".
-      simpl. iApply (IT_tick_err_ne). by iApply internal_eq_sym.
+      simpl. iDestruct (internal_eq_sym with "Hs") as "Hs".
+      by iApply (IT_tick_err_ne with "Hs").
     - rewrite reify_vis_eq_ctx_indep; last first.
       { by rewrite Hre. }
       iIntros "Hr". simpl.
diff --git a/theories/gitree/subofe.v b/theories/gitree/subofe.v
index d6dcb6c..fe571d9 100644
--- a/theories/gitree/subofe.v
+++ b/theories/gitree/subofe.v
@@ -1,6 +1,6 @@
 (* SubOfe: a typeclass for working with generalized return type "a la carte" *)
 From iris.prelude Require Import options.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From gitrees Require Import prelude gitree.core.
 
 Class SubOfe (A B : ofe) :=
@@ -38,7 +38,7 @@ Section it_subofe.
   Definition Ret : A -n> IT := Ret ◎ subOfe_in ◎ inlO.
   Program Definition RetV : A -n> ITV E B := OfeMor RetV ◎ subOfe_in ◎ inlO.
 
-  Lemma Ret_inj (k m : A) {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma Ret_inj (k m : A) {PROP : bi} `{!Sbi PROP} :
     (k ≡ m ⊣⊢ (Ret k ≡ Ret m : PROP))%I.
   Proof.
     iSplit.
@@ -53,7 +53,7 @@ Section it_subofe.
       by iPoseProof (sum_equivI with "H") as "H".
   Qed.
 
-  Lemma RetV_inj (k m : A) {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma RetV_inj (k m : A) {PROP : bi} `{!Sbi PROP} :
     (k ≡ m ⊣⊢ (RetV k ≡ RetV m : PROP))%I.
   Proof.
     iSplit.
@@ -68,36 +68,32 @@ Section it_subofe.
       done.
   Qed.
 
-  Lemma IT_ret_tau_ne k α {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_ret_tau_ne k α {PROP : bi} `{!Sbi PROP} :
     (Ret k ≡ Tau α ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
-    iApply IT_ret_tau_ne.
-    iApply "H1".
+    iApply (IT_ret_tau_ne with "H1").
   Qed.
 
-  Lemma IT_ret_vis_ne n op i k {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_ret_vis_ne n op i k {PROP : bi} `{!Sbi PROP} :
     (Ret n ≡ Vis op i k ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
-    iApply IT_ret_vis_ne.
-    iApply "H1".
+    iApply (IT_ret_vis_ne with "H1").
   Qed.
 
-  Lemma IT_ret_fun_ne k f {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_ret_fun_ne k f {PROP : bi} `{!Sbi PROP} :
     (Ret k ≡ Fun f ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
-    iApply IT_ret_fun_ne.
-    iApply "H1".
+    iApply (IT_ret_fun_ne with "H1").
   Qed.
 
-  Lemma IT_ret_err_ne n e {PROP : bi} `{!BiInternalEq PROP} :
+  Lemma IT_ret_err_ne n e {PROP : bi} `{!Sbi PROP} :
     (Ret n ≡ Err e ⊢ False : PROP)%I.
   Proof.
     iIntros "H1".
-    iApply IT_ret_err_ne.
-    iApply "H1".
+    iApply (IT_ret_err_ne with "H1").
   Qed.
 
   Definition get_ret (f : A -n> IT) : IT -n> IT := get_ret (sumO_rec f Err1 ◎ subOfe_in^-1).
diff --git a/theories/gitree/weakestpre.v b/theories/gitree/weakestpre.v
index fde3d8d..e96dfbb 100644
--- a/theories/gitree/weakestpre.v
+++ b/theories/gitree/weakestpre.v
@@ -1,11 +1,11 @@
 From iris.algebra Require Import list.
 From iris.algebra.lib Require Import excl_auth.
-From iris.proofmode Require Import base tactics classes modality_instances.
+From iris.proofmode Require Import base proofmode classes modality_instances.
 From iris.base_logic.lib Require Export own fancy_updates invariants.
 From gitrees Require Import prelude.
 From gitrees.gitree Require Import core reify greifiers reductions.
 
-Lemma cons_internal_equiv_tail {PROP : bi} `{!BiInternalEq PROP}
+Lemma cons_internal_equiv_tail {PROP : bi} `{!Sbi PROP}
   {X : ofe} `{!Cofe X}
   (x y : listO X) a b :
   ⊢@{PROP} a :: x ≡ b :: y
@@ -15,7 +15,7 @@ Proof.
   by iApply (f_equivI tail (a :: x) (b :: y)).
 Qed.
 
-Lemma cons_internal_equiv_head {PROP : bi} `{!BiInternalEq PROP}
+Lemma cons_internal_equiv_head {PROP : bi} `{!Sbi PROP}
   {X : ofe} `{!Cofe X}
   (x y : listO X) a b :
   ⊢@{PROP} a :: x ≡ b :: y
@@ -27,7 +27,7 @@ Proof.
   by rewrite option_equivI.
 Qed.
 
-Lemma app_internal_equiv_app {PROP : bi} `{!BiInternalEq PROP}
+Lemma app_internal_equiv_app {PROP : bi} `{!Sbi PROP}
   {X : ofe} `{!Cofe X}
   (x1 x2 y1 y2 : listO X) :
   ⊢@{PROP} x1 ++ x2 ≡ y1 ++ y2
@@ -454,17 +454,31 @@ Section weakestpre.
   Qed.
   Next Obligation.
     rewrite /not_stuck.
-    intros ?????? [] ?; simpl.
-    f_equiv; first solve_proper.
-    f_equiv.
-    f_equiv; intros ?.
-    f_equiv; intros p.
-    do 3 f_equiv.
-    do 3 (f_equiv; intros ?).
-    do 5 f_equiv.
-    induction (num_later_per_step p).
-    - solve_proper.
-    - solve_proper.
+    intros ?????? [] α; simpl.
+    apply bi.or_ne.
+    - apply bi.exist_ne=> αv.
+      apply bi.and_ne; first reflexivity.
+      apply fupd_ne. apply H.
+    - apply bi.and_ne; first reflexivity.
+      apply bi.forall_ne=> σ.
+      apply bi.forall_ne=> ns.
+      apply bi.wand_ne; first reflexivity.
+      apply fupd_ne.
+      apply bi.and_ne; first reflexivity.
+      apply bi.forall_ne=> σ'.
+      apply bi.forall_ne=> β.
+      apply bi.forall_ne=> en.
+      apply bi.wand_ne; first reflexivity.
+      do 3 f_equiv.
+      apply fupd_ne.
+      induction (num_later_per_step ns) as [|k IH]; simpl.
+      + apply fupd_ne.
+        apply bi.sep_ne; first reflexivity.
+        apply bi.sep_ne.
+        * pose proof (@ofe_mor_ne _ _ _ self n0 x y H) as Hself.
+          exact (Hself (x0 ↾ i) β).
+        * apply big_sepL_ne=> j ef. reflexivity.
+      + do 3 f_equiv. apply IH.
   Qed.
 
   #[local] Instance wp_pre_contractive s : Contractive (wp_pre s).
@@ -539,7 +553,7 @@ Section weakestpre.
       f_contractive.
       do 4 f_equiv.
       + apply IH; eauto.
-        eapply dist_le; [apply Hp|lia].
+        eapply (dist_le m m0); [exact Hp|by apply SIdx.lt_le_incl].
       + do 3 f_equiv.
         unfold wp.
         do 3 f_equiv.
@@ -875,7 +889,7 @@ Section weakestpre.
     iSplit.
     { iRight. eauto with iFrame. }
     iIntros (σ' β en) "Hst". iExFalso.
-    iApply internal_step_err. done.
+    iApply (internal_step_err rG σ e β σ'). done.
   Qed.
 
   Lemma wp_stuckness_mono α E1 (s1 s2 : error → Prop) Φ :
@@ -1230,7 +1244,7 @@ Section weakestpre.
     iModIntro.
     iApply (step_fupdN_wand with "J").
     iIntros ">(%nt & J1 & J2 & J3)".
-    eapply elem_of_list_lookup in HIn as [i Hlook].
+    eapply list_elem_of_lookup in HIn as [i Hlook].
     destruct ((Ψs ++ replicate nt fork_post) !! i) as [Φ|] eqn: Hlook2; last first.
     {
       rewrite /wptp big_sepL2_alt. iDestruct "J3" as "[%Hlen J3]". exfalso.
@@ -1756,31 +1770,24 @@ Section weakestpre_lifting.
   Proof.
     destruct a.
     - iIntros "H".
-      iApply wp_reify_idx_ctx_dep.
+      iApply wp_subreify_ctx_dep'.
       iMod "H" as (σ y σ' β l) "[Hlst [#Hreify [#Hk H]]]".
       iModIntro.
-      iExists (sR_state σ), (k (subEff_outs y)).
-      iExists _, β, l.
-      iSplitL "Hlst".
-      { iFrame "Hlst". }
-      iSplitR "Hk H"; first last.
+      iExists σ, (k (subEff_outs y)), σ', β, l.
+      iFrame "Hlst".
+      iSplitR "Hk H".
       {
-        iFrame "Hk".
-        iApply "H".
+        Opaque prodO_map.
+        simpl.
+        iRewrite "Hreify".
+        Transparent prodO_map.
+        simpl.
+        iPureIntro.
+        do 3 f_equiv.
       }
-      epose proof (subReifier_reify_idxI_ctx_dep (Σ := Σ)
-                     (sReifier_NotCtxDep_min sR CtxDep) op x (k (subEff_outs y))
-                     (k ◎ subEff_outs) σ σ') as G.
-      assert (k ≡ k ◎ ofe_iso_1 subEff_outs ◎ subEff_outs ^-1) as ->.
-      { intro; simpl; by rewrite ofe_iso_12. }
-      iApply G.
-      Opaque prodO_map.
-      simpl.
-      iRewrite "Hreify".
-      Transparent prodO_map.
-      simpl.
-      iPureIntro.
-      do 3 f_equiv.
+      iSplit; first done.
+      iNext. iIntros "Hlc Hs".
+      by iApply ("H" with "Hlc Hs").
     - iApply wp_subreify_ctx_indep'.
   Qed.
 
@@ -1931,7 +1938,12 @@ Proof.
     + iApply (internal_step_tp_internal_step _ _ _ _ _ t1 t2 with "H2").
     + iSpecialize ("IH" $! γ σ'' β σ' l'' t1 (t2 ++ l')).
       rewrite -app_assoc.
-      iRewrite - "H1" in "IH".
+      iDestruct (internal_eq_sym with "H1") as "H1sym".
+      iApply (internal_eq_rewrite (PROP := iProp Σ) (l' ++ l'') l
+                (λ l0, tp_internal_steps (A := A) (gReifiers_sReifier rs)
+                  (t1 ++ γ :: t2 ++ l') σ''
+                  (t1 ++ β :: t2 ++ l0) σ' k)%I with "H1sym").
+      { solve_proper. }
       iApply "IH".
       iApply "H3".
 Qed.
@@ -1982,7 +1994,7 @@ Proof.
   {
     intros [Hprf | [Hprf | Hprf]%Hdisj]%Hdisj.
     - left.
-      eapply uPred.pure_soundness.
+      eapply (sbi.pure_soundness (PROP:=iProp Σ)).
       by iPoseProof (Hprf) as "H".
     - right. left.
       apply (internal_step_safe_external_step _ (Σ:=Σ)).
@@ -1992,24 +2004,24 @@ Proof.
       destruct (IT_dont_confuse β)
         as [[e Ha] | [[m Ha] | [ [g Ha] | [[α' Ha]|[op [i [ko Ha]]]] ]]].
       + exists e. split; eauto.
-        eapply uPred.pure_soundness.
+        eapply (sbi.pure_soundness (PROP:=iProp Σ)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (e') "[He %Hs]". rewrite Ha.
         iPoseProof (Err_inj' with "He") as "%He".
         iPureIntro. rewrite He//.
-      + exfalso. eapply uPred.pure_soundness.
+      + exfalso. eapply (sbi.pure_soundness (PROP:=iProp Σ)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (e') "[Ha Hs]". rewrite Ha.
         iApply (IT_ret_err_ne with "Ha").
-      + exfalso. eapply uPred.pure_soundness.
+      + exfalso. eapply (sbi.pure_soundness (PROP:=iProp Σ)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (e') "[Ha Hs]". rewrite Ha.
         iApply (IT_fun_err_ne with "Ha").
-      + exfalso. eapply uPred.pure_soundness.
+      + exfalso. eapply (sbi.pure_soundness (PROP:=iProp Σ)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (e') "[Ha Hs]". rewrite Ha.
         iApply (IT_tick_err_ne with "Ha").
-      + exfalso. eapply uPred.pure_soundness.
+      + exfalso. eapply (sbi.pure_soundness (PROP:=iProp Σ)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (e') "[Ha Hs]". rewrite Ha.
         iApply (IT_vis_err_ne with "Ha").
@@ -2027,15 +2039,20 @@ Proof.
                    state_interp_fun_ne
                    state_interp_fun_decomp)
                   "(Haux & H)".
+  pose Hgs := @GitreeG n a rs A _ Σ Hinv sg
+                state_interp_fun aux_interp_fun fork_post fork_post_ne
+                num_later_per_step state_interp_fun_mono
+                state_interp_fun_ne state_interp_fun_decomp.
   iPoseProof ("H" with "[$Hs2 $Hcred1]") as "Hic".
   iDestruct (state_interp_fun_decomp with "[$Hs $Haux]") as "Hs".
   iPoseProof (external_steps_internal_steps _ _ _ _ _ _ _ Hstep) as "Hsteps".
   iDestruct (internal_steps_to_tp_internal_steps _ _ _ _ _ _ _ _ _ [] [] with "Hsteps") as "Hsteps'".
-  iAssert (wptp rs s [α] [Φ])%I with "[Hic]" as "Hwp".
-  { by iApply big_sepL2_singleton. }
+  iAssert (wptp rs s [α] ([Φ] : list (ITV -d> iProp Σ)))%I with "[Hic]" as "Hwp".
+  { rewrite /wptp big_sepL2_singleton. iExact "Hic". }
   assert (β ∈ β :: l) as Hin.
   { set_solver. }
-  iMod (wp_tp_internal_steps_progress rs [α] σ β (β :: l) σ' k s cr [Φ] Hin
+  iMod (wp_tp_internal_steps_progress rs [α] σ β (β :: l) σ' k s cr
+          ([Φ] : list (ITV -d> iProp Σ)) Hin
          with "[$Hsteps' $Hwp $Hcred2 $Hs]") as "J".
   iModIntro.
   rewrite step_fupdN_S_fupd /=.
@@ -2096,7 +2113,7 @@ Proof.
     apply Hdisj in Hprf'.
     destruct Hprf' as [Hprf | [Hprf | Hprf]%Hdisj].
     - left.
-      eapply uPred.pure_soundness.
+      eapply (sbi.pure_soundness (PROP:=iProp Σ)).
       by iPoseProof (Hprf) as "H".
     - right. left.
       apply (internal_step_safe_external_step _ (Σ:=Σ)).
@@ -2106,24 +2123,24 @@ Proof.
       destruct (IT_dont_confuse e2)
         as [[e Ha] | [[m Ha] | [ [g Ha] | [[α' Ha]|[op [i [ko Ha]]]] ]]].
       + exists e. split; eauto.
-        eapply uPred.pure_soundness.
+        eapply (sbi.pure_soundness (PROP:=iProp Σ)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (e') "[He %Hs]". rewrite Ha.
         iPoseProof (Err_inj' with "He") as "%He".
         iPureIntro. rewrite He//.
-      + exfalso. eapply uPred.pure_soundness.
+      + exfalso. eapply (sbi.pure_soundness (PROP:=iProp Σ)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (e') "[Ha Hs]". rewrite Ha.
         iApply (IT_ret_err_ne with "Ha").
-      + exfalso. eapply uPred.pure_soundness.
+      + exfalso. eapply (sbi.pure_soundness (PROP:=iProp Σ)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (e') "[Ha Hs]". rewrite Ha.
         iApply (IT_fun_err_ne with "Ha").
-      + exfalso. eapply uPred.pure_soundness.
+      + exfalso. eapply (sbi.pure_soundness (PROP:=iProp Σ)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (e') "[Ha Hs]". rewrite Ha.
         iApply (IT_tick_err_ne with "Ha").
-      + exfalso. eapply uPred.pure_soundness.
+      + exfalso. eapply (sbi.pure_soundness (PROP:=iProp Σ)).
         iPoseProof (Hprf) as "H".
         iDestruct "H" as (e') "[Ha Hs]". rewrite Ha.
         iApply (IT_vis_err_ne with "Ha").
@@ -2148,10 +2165,11 @@ Proof.
   iPoseProof ("H" with "[$Hs2 $Hcred1]") as "Hic".
   iDestruct (state_interp_fun_decomp with "[$Hs $Haux]") as "Hs".
   iPoseProof (tp_external_steps_tp_internal_steps _ _ _ _ _ _ Hstep) as "Hsteps".
-  iAssert (wptp rs s [α] [Φ])%I with "[Hic]" as "Hwp".
-  { by iApply big_sepL2_singleton. }
+  iAssert (wptp rs s [α] ([Φ] : list (ITV -d> iProp Σ)))%I with "[Hic]" as "Hwp".
+  { rewrite /wptp big_sepL2_singleton. iExact "Hic". }
   
-  iMod (wp_tp_internal_steps_progress rs [α] σ e2 β σ' k s cr [Φ] HIn
+  iMod (wp_tp_internal_steps_progress rs [α] σ e2 β σ' k s cr
+          ([Φ] : list (ITV -d> iProp Σ)) HIn
                with "[$Hsteps $Hwp $Hcred2 $Hs]") as "J".
   rewrite step_fupdN_S_fupd /=.
   iApply (step_fupdN_wand with "J").
@@ -2211,7 +2229,7 @@ Lemma wp_adequacy_tp cr (num_later_per_step : nat → nat)
 Proof.
   intros rg F IT' ITV' Hprf.
   cut (⊢ ⌜ψ⌝ : iProp Σ)%I.
-  { intros HH. eapply uPred.pure_soundness; eauto. }
+  { intros HH. eapply sbi.pure_soundness; eauto. }
   eapply (step_fupdN_soundness_lc _ (steps_sum num_later_per_step cr k)
             (cr + steps_sum num_later_per_step cr k)).
   intros Hinv. iIntros "(Hfuel & Hcred)".
@@ -2263,8 +2281,9 @@ Proof.
   clear Hinv sg state_interp_fun state_interp_fun_ne aux_interp_fun fork_post fork_post_ne
     state_interp_fun_mono state_interp_fun_decomp.
 
-  unshelve iApply (step_fupdN_soundness_lc _ (S (steps_sum num_later_per_step cr k))
-            (cr + steps_sum num_later_per_step cr k)); first apply _.
+  iApply (@step_fupdN_soundness_lc Σ _ (not_stuck rs s e2 σ') _
+            (S (steps_sum num_later_per_step cr k))
+            (cr + steps_sum num_later_per_step cr k)).
   intros Hinv. iIntros "(Hfuel & Hcred)".
   iMod (new_state_interp σ) as (sg) "[Hs Hs2]".
   iMod (Hprf Hinv sg) as (state_interp_fun
@@ -2289,6 +2308,8 @@ Proof.
   iModIntro.
   iIntros ">J".
   by iFrame "J".
+  Unshelve.
+  all: try solve [apply _].
 Qed.
 
 Lemma wp_adequacy cr (num_later_per_step : nat → nat)
diff --git a/theories/hom.v b/theories/hom.v
index c906898..f78d4ca 100644
--- a/theories/hom.v
+++ b/theories/hom.v
@@ -31,7 +31,7 @@ Section hom.
       + by intros f x.
       + by intros f g ? x.
       + by intros f g h ?? x; trans (g x).
-    - intros n m f g ? x ?; eauto using dist_le with si_solver.
+    - intros n m f g ? x ?; eauto using dist_le.
   Qed.
   Canonical Structure HOM := Ofe HOM_Type HOM_ofe_mixin.
 
diff --git a/theories/lang_generic.v b/theories/lang_generic.v
index e1d6ef1..cf058fe 100644
--- a/theories/lang_generic.v
+++ b/theories/lang_generic.v
@@ -274,11 +274,11 @@ Section tm_interp_fin.
       intros [x | x].
       - rewrite !elem_of_list_to_set.
         intros _ H2.
-        apply elem_of_list_fmap_2 in H2.
+        apply list_elem_of_fmap_1 in H2.
         destruct H2 as [y [H2 H2']]; inversion H2.
       - rewrite !elem_of_list_to_set.
         intros H1 _.
-        apply elem_of_list_fmap_2 in H1.
+        apply list_elem_of_fmap_1 in H1.
         destruct H1 as [y [H1 H1']]; inversion H1.
     }
     iDestruct "H" as "(H1 & H2)".
@@ -316,7 +316,7 @@ Section tm_interp_fin.
       intros [| x].
       - rewrite !elem_of_list_to_set.
         intros _ H2.
-        apply elem_of_list_fmap_2 in H2.
+        apply list_elem_of_fmap_1 in H2.
         destruct H2 as [y [H2 H2']]; inversion H2.
       - rewrite !elem_of_list_to_set.
         intros H1 _.
diff --git a/theories/lib/eq.v b/theories/lib/eq.v
index b3786fd..80dfea1 100644
--- a/theories/lib/eq.v
+++ b/theories/lib/eq.v
@@ -70,7 +70,8 @@ Section ofe_decision.
     by apply eqb_prop in H.
   Qed.
   Next Obligation.
-    intros ?? ->; simpl.
+    intros a b. simpl.
+    intros H. rewrite H.
     apply eqb_reflx.
   Qed.
   Next Obligation.
@@ -309,6 +310,46 @@ Section decidable_equality.
     : IT -n> IT -n> IT := λne a b, safe_compare_def a b.
   Solve All Obligations with solve_proper.
 
+  Local Lemma ret_true_err_false e : ¬ ((Err e : IT) ≡ Ret true).
+  Proof using A AC E SO Σ.
+    intros H.
+    eapply (sbi.pure_soundness (PROP:=iProp)).
+    iAssert ((Err e : IT) ≡ Ret true)%I as "H".
+    { by iPureIntro. }
+    iApply (IT_ret_err_ne (E:=E) (A:=boolO) (B:=A) true e).
+    iSymmetry. iExact "H".
+  Qed.
+
+  Local Lemma ret_false_true_false : ¬ ((Ret false : IT) ≡ Ret true).
+  Proof using A AC E SO Σ.
+    intros H.
+    eapply (sbi.pure_soundness (PROP:=iProp)).
+    iAssert ((Ret false : IT) ≡ Ret true)%I as "H".
+    { by iPureIntro. }
+    iDestruct (Ret_inj with "H") as "%G".
+    inversion G.
+  Qed.
+
+  Local Lemma ret_true_tick_false α : ¬ ((Tick α : IT) ≡ Ret true).
+  Proof using A AC E SO Σ.
+    intros H.
+    eapply (sbi.pure_soundness (PROP:=iProp)).
+    iAssert ((Tick α : IT) ≡ Ret true)%I as "H".
+    { by iPureIntro. }
+    iApply (IT_ret_tau_ne (E:=E) (A:=boolO) (B:=A) true).
+    iSymmetry. iExact "H".
+  Qed.
+
+  Local Lemma ret_true_vis_false op i ko : ¬ ((Vis op i ko : IT) ≡ Ret true).
+  Proof using A AC E SO Σ.
+    intros H.
+    eapply (sbi.pure_soundness (PROP:=iProp)).
+    iAssert ((Vis op i ko : IT) ≡ Ret true)%I as "H".
+    { by iPureIntro. }
+    iApply (IT_ret_vis_ne (E:=E) (A:=boolO) (B:=A) true).
+    iSymmetry. iExact "H".
+  Qed.
+
   Lemma safe_compare_reflect x y : safe_compare x y ≡ Ret true → x ≡ y.
   Proof using A AC SO dec Σ.
     destruct (IT_dont_confuse x)
@@ -316,12 +357,7 @@ Section decidable_equality.
     - intros H.
       rewrite /safe_compare /= Ha in H.
       rewrite /safe_compare_def get_val_err in H.
-      exfalso.
-      symmetry in H.
-      assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-      iApply IT_ret_err_ne.
-      rewrite <-H.
-      done.
+      by exfalso; eapply ret_true_err_false.
     - intros H.
       rewrite /safe_compare /= Ha in H.
       rewrite /safe_compare_def in H.
@@ -330,11 +366,7 @@ Section decidable_equality.
       + rewrite core.get_val_ret /= in H.
         rewrite Ha' in H.
         rewrite get_val_err in H.
-        exfalso.
-        assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-        iApply IT_ret_err_ne.
-        rewrite ->H.
-        done.
+        by exfalso; eapply ret_true_err_false.
       + rewrite core.get_val_ret /= in H.
         rewrite Ha' in H.
         rewrite core.get_val_ret /= in H.
@@ -345,100 +377,44 @@ Section decidable_equality.
           rewrite Heq in Ha.
           by rewrite -Ha' in Ha.
         * exfalso.
-          assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-          iAssert (false ≡ true)%I as "%G".
-          {
-            iApply Ret_inj.
-            rewrite <-H.
-            done.
-          }
-          inversion G.
+          by eapply ret_false_true_false.
       + rewrite core.get_val_ret /= in H.
         rewrite Ha' in H.
         rewrite get_val_fun /= in H.
         rewrite get_unboxed_ret_ret /= in H.
         rewrite get_unboxed_ret_fun /= in H.
-        exfalso.
-        assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-        iDestruct (Ret_inj with "[]") as "H".
-        { iPureIntro. apply H. }
-        iDestruct "H" as "%G".
-        Unshelve.
-        2: apply _.
-        inversion G.
+        by exfalso; eapply ret_false_true_false.
       + rewrite core.get_val_ret /= in H.
         rewrite Ha' in H.
         rewrite get_val_tick /= in H.
-        exfalso.
-        assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-        iApply IT_ret_tick_ne.
-        rewrite ->H.
-        done.
+        by exfalso; eapply ret_true_tick_false.
       + rewrite core.get_val_ret /= in H.
         rewrite Ha' in H.
         rewrite get_val_vis /= in H.
-        exfalso.
-        assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-        iApply IT_ret_vis_ne.
-        rewrite ->H.
-        done.
+        by exfalso; eapply ret_true_vis_false.
     - intros H.
       rewrite /safe_compare /= /safe_compare_def /= Ha get_val_fun /= in H.
       destruct (IT_dont_confuse y)
         as [[e' Ha'] | [[m' Ha'] | [ [g' Ha'] | [[α'' Ha']|[op' [i' [ko' Ha']]]] ]]].
       + rewrite Ha' get_val_err in H.
-        exfalso.
-        assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-        iApply IT_ret_err_ne.
-        rewrite ->H.
-        done.
+        by exfalso; eapply ret_true_err_false.
       + rewrite Ha' core.get_val_ret /= in H.
         rewrite get_unboxed_ret_fun /= in H.
-        exfalso.
-        assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-        iDestruct (Ret_inj with "[]") as "H".
-        { iPureIntro. apply H. }
-        iDestruct "H" as "%G".
-        Unshelve.
-        2: apply _.
-        inversion G.        
+        by exfalso; eapply ret_false_true_false.
       + rewrite Ha' get_val_fun /= in H.
         rewrite get_unboxed_ret_fun in H.
-        exfalso.
-        assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-        iDestruct (Ret_inj with "[]") as "H".
-        { iPureIntro. apply H. }
-        iDestruct "H" as "%G".
-        Unshelve.
-        2: apply _.
-        inversion G.
+        by exfalso; eapply ret_false_true_false.
       + rewrite Ha' get_val_tick /= in H.
-        exfalso.
-        assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-        iApply IT_ret_tick_ne.
-        rewrite ->H.
-        done.
+        by exfalso; eapply ret_true_tick_false.
       + rewrite Ha' in H.
         rewrite get_val_vis /= in H.
-        exfalso.
-        assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-        iApply IT_ret_vis_ne.
-        rewrite ->H.
-        done.
+        by exfalso; eapply ret_true_vis_false.
     - intros H.
       rewrite /safe_compare /= /safe_compare_def /= Ha get_val_tick /= in H.
-      exfalso.
-      assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-      iApply IT_ret_tick_ne.
-      rewrite ->H.
-      done.
+      by exfalso; eapply ret_true_tick_false.
     - intros H.
       rewrite /safe_compare /= /safe_compare_def /= Ha get_val_vis /= in H.
-      exfalso.
-      assert (⊢@{iProp} False)%I; last by eapply uPred.pure_soundness.
-      iApply IT_ret_vis_ne.
-      rewrite ->H.
-      done.
+      by exfalso; eapply ret_true_vis_false.
   Qed.
 
   Lemma safe_compare_ret x y : safe_compare (Ret x) (Ret y) ≡ Ret (ofe_decision x y).
diff --git a/theories/lib/factorial.v b/theories/lib/factorial.v
index a24ce3e..0c2e134 100644
--- a/theories/lib/factorial.v
+++ b/theories/lib/factorial.v
@@ -47,8 +47,9 @@ Section fact.
     iNext. iNext. iIntros "Hl".
     iApply wp_val. iModIntro.
     unfold IFSCtx. simpl.
-    iAssert ((IT_of_V (E:=F) (RetV n)) ≡ (Ret n))%I as "#Hn".
-    { iPureIntro. apply (IT_of_V_Ret (B:=R)). }
+    iAssert ((IT_of_V (E:=F) (RetV (E:=F) (A:=natO) (B:=R) n))
+               ≡ (Ret (E:=F) (A:=natO) (B:=R) n))%I as "#Hn".
+    { iPureIntro. apply (@IT_of_V_Ret F natO R _ _ n). }
     iRewrite "Hn".
     destruct n as [|n].
     - rewrite IF_False ; last lia.
@@ -67,14 +68,16 @@ Section fact.
       iNext. iNext. iIntros "Hacc".
       iApply wp_val. iModIntro.
       simpl. unfold NatOpRSCtx.
-      iAssert (IT_of_V (E:=F) (RetV m) ≡ (Ret m))%I as "#Hm".
-      { iPureIntro. apply (IT_of_V_Ret (B:=R)). }
+      iAssert (IT_of_V (E:=F) (RetV (E:=F) (A:=natO) (B:=R) m)
+                  ≡ (Ret (E:=F) (A:=natO) (B:=R) m))%I as "#Hm".
+      { iPureIntro. apply (@IT_of_V_Ret F natO R _ _ m). }
       iRewrite "Hm".
       rewrite NATOP_Ret.
       iApply wp_val. iModIntro.
       iApply wp_let.
-      iAssert (IT_of_V (E:=F) (RetV (S n)) ≡ (Ret (S n)))%I as "#Hsn".
-      { iPureIntro. apply (IT_of_V_Ret (B:=R)). }
+      iAssert (IT_of_V (E:=F) (RetV (E:=F) (A:=natO) (B:=R) (S n))
+                  ≡ (Ret (E:=F) (A:=natO) (B:=R) (S n)))%I as "#Hsn".
+      { iPureIntro. apply (@IT_of_V_Ret F natO R _ _ (S n)). }
       iRewrite "Hsn".
       rewrite NATOP_Ret.
       iApply wp_val. iModIntro.
diff --git a/theories/lib/generators.v b/theories/lib/generators.v
index eed5126..a9a5288 100644
--- a/theories/lib/generators.v
+++ b/theories/lib/generators.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import classes tactics.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import classes proofmode.
+From iris.bi Require Import algebra.
 From iris.heap_lang Require Export locations.
 From gitrees Require Import prelude.
 From gitrees Require Import gitree gitree.lambda.
@@ -49,7 +49,7 @@ Section lib.
   Local Instance rec_val body : IntoVal (rec body) (recV body).
   Proof.
     rewrite /IntoVal.
-    apply bi.siProp.internal_eq_soundness.
+    apply (@bi.internal_eq.internal_eq_soundness siProp _).
     iLöb as "IH".
     iEval (rewrite rec_unfold recV_unfold).
     iApply f_equivI.
diff --git a/theories/prelude.v b/theories/prelude.v
index ee89b73..e69d5a0 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -4,7 +4,7 @@ From iris.prelude Require Export options prelude.
 From iris.algebra Require Import list ofe local_updates.
 From iris.bi Require Import notation.
 From iris.si_logic Require Import bi siprop.
-From iris.proofmode Require Import classes tactics modality_instances
+From iris.proofmode Require Import classes proofmode modality_instances
                                    coq_tactics reduction.
 
 Definition sum_map' {A B C : Set} (f : A → C) (g : B → C) : sum A B → C :=
@@ -34,11 +34,11 @@ Coercion ofe_iso_1' : ofe_iso >-> Funclass.
 Notation "f ^-1" := (ofe_iso_2 f) (at level 20) : function_scope.
 
 #[export] Instance optionO_map_proper (A B : ofe) :
-  Proper ((≡) ==> (≡)) (@optionO_map A B).
+  Proper ((≡) ==> (≡)) (@optionO_map _ A B).
 Proof. solve_proper. Qed.
 
 #[export] Instance prodO_map_proper (A B C D : ofe) :
-  Proper ((≡) ==> (≡) ==> (≡)) (@prodO_map A B C D).
+  Proper ((≡) ==> (≡) ==> (≡)) (@prodO_map _ A B C D).
 Proof.
   intros ?? H ?? G [a b]; simpl.
   f_equiv; solve_proper.
@@ -62,9 +62,9 @@ Program Definition later_ap {A B} (f : later (A -n> B)) : laterO A -n> laterO B
   λne x, Next $ (later_car f) (later_car x).
 #[export] Instance later_ap_ne {A B} : NonExpansive (@later_ap A B).
 Proof.
-  intros n f g Hfg. intros x. simpl.
-  eapply Next_contractive. destruct n; eauto using dist_later_0, dist_later_S.
-  apply dist_later_S. f_equiv. eapply later_car_anti_contractive; eauto.
+  intros n f g [Hfg]. intros x. simpl.
+  eapply Next_contractive. split. intros m Hm.
+  f_equiv. by apply Hfg.
 Qed.
 Definition laterO_ap {A B} := OfeMor (@later_ap A B).
 
@@ -178,18 +178,10 @@ Qed.
 
 Section siProp.
 Import siprop.
-Import siProp_primitive.
-Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
-  unfold bi_pure, bi_entails, bi_later,
-    bi_and, bi_or, bi_impl, bi_forall, bi_exist,
-    bi_sep, bi_wand, bi_persistently, bi_later; simpl;
-  unfold internal_eq, bi_internal_eq_internal_eq,
-    plainly, bi_plainly_plainly; simpl;
-  siProp_primitive.unseal.
 Lemma internal_eq_pointwise {A B : ofe} (f g : A -n> B) :
   ⊢@{bi.siPropI} (∀ x, f x ≡ g x) → f ≡ g.
 Proof.
-  unseal. split. intros n _ m Hnm H x. apply H.
+  rewrite -ofe_morO_equivI. auto.
 Qed.
 End siProp.
 
@@ -214,9 +206,14 @@ Local Ltac iRewriteFindPred :=
      match goal with |- (∀ y, @?Ψ y ⊣⊢ _) => unify Φ Ψ; reflexivity end
   end.
 
+Local Ltac solve_iRewrite_ne :=
+  solve [ intros ??? ->; reflexivity
+        | timeout 3 (repeat intro; simpl; repeat f_equiv; eauto)
+        | timeout 3 solve_proper ].
+
 Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
   iPoseProofCore lem as true (fun Heq =>
-    eapply (tac_rewrite _ Heq _ _ lr);
+    notypeclasses refine (tac_rewrite _ Heq _ _ lr _ _ _ _ _ _ _ _ _);
       [pm_reflexivity ||
        let Heq := pretty_ident Heq in
        fail "iRewrite:" Heq "not found"
@@ -224,7 +221,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
        let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
        fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
-      | solve [ intros ??? ->; reflexivity | solve_proper ] (** THIS IS CHANGED *)
+      | solve_iRewrite_ne
       |pm_prettify; iClearHyp Heq]).
 
 Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore Right lem.
@@ -232,7 +229,7 @@ Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore Left lem.
 
 Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
   iPoseProofCore lem as true (fun Heq =>
-    eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
+    notypeclasses refine (tac_rewrite_in _ Heq _ _ H _ _ lr _ _ _ _ _ _ _ _ _ _);
       [pm_reflexivity ||
        let Heq := pretty_ident Heq in
        fail "iRewrite:" Heq "not found"
@@ -243,7 +240,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
        let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
        fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
-      | solve [ intros ??? ->; reflexivity | solve_proper ] (** THIS IS CHANGED *)
+      | solve_iRewrite_ne
       |pm_reduce; pm_prettify; iClearHyp Heq]).
 
 Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
@@ -251,6 +248,11 @@ Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
 Tactic Notation "iRewrite" "-" open_constr(lem) "in" constr(H) :=
   iRewriteCore Left lem in H.
 
+Tactic Notation "iSymmetry" :=
+  iApply internal_eq_sym.
+Tactic Notation "iSymmetry" "in" constr(H) :=
+  iDestruct (internal_eq_sym with H) as H.
+
 (** Beefed up solve_proper *)
 Ltac solve_proper_please := repeat (repeat intro; simpl; repeat f_equiv); solve_proper.
 
diff --git a/theories/utils/ghost_stacks.v b/theories/utils/ghost_stacks.v
index 1bc9853..06a2175 100644
--- a/theories/utils/ghost_stacks.v
+++ b/theories/utils/ghost_stacks.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import auth gmap gset excl frac.
 From iris.base_logic Require Import invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.bi.lib Require Import fractional.
 
 Definition ghost_id := gname.
@@ -191,12 +191,12 @@ Section ghost_stacks.
     iDestruct "Hgs" as "(%&$&Hgs)".
     replace M with (delete n M ∪ {[n := s]}); last first.
     { apply map_eq; intros i; destruct (decide (i = n)) as [->|].
-      - rewrite lookup_union lookup_singleton lookup_delete //.
+      - rewrite lookup_union lookup_singleton_eq lookup_delete_eq //.
       - rewrite lookup_union lookup_singleton_ne // lookup_delete_ne //.
         case: (M !! i); done. }
     assert (delete n M ##ₘ {[n := s]}).
     { apply map_disjoint_spec; intros i ? ? Hdl [-> ->]%lookup_singleton_Some.
-      rewrite lookup_delete in Hdl; done. }
+      rewrite lookup_delete_eq in Hdl; done. }
     repeat (rewrite big_sepM_union; last done).
     rewrite !big_sepM_singleton.
     rewrite bool_decide_eq_false_2; last set_solver.
@@ -224,12 +224,12 @@ Section ghost_stacks.
     iSplit; first by iPureIntro; set_solver.
     replace M with (delete n M ∪ {[n := s]}); last first.
     { apply map_eq; intros i; destruct (decide (i = n)) as [->|].
-      - rewrite lookup_union lookup_singleton lookup_delete //.
+      - rewrite lookup_union lookup_singleton_eq lookup_delete_eq //.
       - rewrite lookup_union lookup_singleton_ne // lookup_delete_ne //.
         case: (M !! i); done. }
     assert (delete n M ##ₘ {[n := s]}).
     { apply map_disjoint_spec; intros i ? ? Hdl [-> ->]%lookup_singleton_Some.
-      rewrite lookup_delete in Hdl; done. }
+      rewrite lookup_delete_eq in Hdl; done. }
     repeat (rewrite big_sepM_union; last done).
     iDestruct "Hgs" as "[Hgs _]".
     rewrite !big_sepM_singleton.
@@ -238,7 +238,7 @@ Section ghost_stacks.
     iApply big_sepM_mono; last iAssumption.
     intros i ? Hnmi; simpl.
     assert (i ≠ n).
-    { intros ->; rewrite lookup_delete in Hnmi; done. }
+    { intros ->; rewrite lookup_delete_eq in Hnmi; done. }
     destruct (decide (i ∈ N)).
     { repeat (rewrite bool_decide_eq_true_2; last set_solver); done. }
     { repeat (rewrite bool_decide_eq_false_2; last set_solver); done. }
@@ -258,19 +258,19 @@ Section ghost_stacks.
     { apply not_elem_of_dom in Heq; set_solver. }
     replace M with (delete n M ∪ {[n := s']}); last first.
     { apply map_eq; intros i; destruct (decide (i = n)) as [->|].
-      - rewrite lookup_union lookup_singleton lookup_delete //.
+      - rewrite lookup_union lookup_singleton_eq lookup_delete_eq //.
       - rewrite lookup_union lookup_singleton_ne // lookup_delete_ne //.
         case: (M !! i); done. }
     assert (delete n M ##ₘ {[n := s']}).
     { apply map_disjoint_spec; intros i ? ? Hdl [-> ->]%lookup_singleton_Some.
-      rewrite lookup_delete in Hdl; done. }
+      rewrite lookup_delete_eq in Hdl; done. }
     replace (<[n:=s]> (delete n M ∪ {[n := s']})) with (delete n M ∪ {[n := s]}); last first.
     { apply map_eq; intros i. destruct (decide (i = n)) as [->|].
-      - rewrite lookup_insert lookup_union lookup_delete lookup_singleton //.
+      - rewrite lookup_insert_eq lookup_union lookup_delete_eq lookup_singleton_eq //.
       - rewrite lookup_insert_ne // !lookup_union !lookup_singleton_ne //. }
     assert (delete n M ##ₘ {[n := s]}).
     { apply map_disjoint_spec; intros i ? ? Hdl [-> ->]%lookup_singleton_Some.
-      rewrite lookup_delete in Hdl; done. }
+      rewrite lookup_delete_eq in Hdl; done. }
     repeat (rewrite big_sepM_union; last done).
     iDestruct "HM" as "[HM _]".
     rewrite !big_sepM_singleton.
@@ -279,7 +279,7 @@ Section ghost_stacks.
     iApply big_sepM_mono; last iAssumption.
     intros i ? Hnmi; simpl.
     assert (i ≠ n).
-    { intros ->; rewrite lookup_delete in Hnmi; done. }
+    { intros ->; rewrite lookup_delete_eq in Hnmi; done. }
     destruct (decide (i ∈ N)).
     { repeat (rewrite bool_decide_eq_true_2; last set_solver); done. }
     { repeat (rewrite bool_decide_eq_false_2; last set_solver); done. }
diff --git a/theories/utils/wbwp.v b/theories/utils/wbwp.v
index ab6a1c1..62073a6 100644
--- a/theories/utils/wbwp.v
+++ b/theories/utils/wbwp.v
@@ -170,7 +170,7 @@ Section wp.
     iDestruct (gstack_full_exists with "Hfl") as "#Hex".
     destruct (M !! m) as [s'|] eqn:HMns'; last by apply not_elem_of_dom in HMns'; set_solver.
     iDestruct (gstacks_out_swap _ _ m s with "HM") as "HM"; first done.
-    iDestruct (gstacks_put_back with "Hfl HM") as "HM"; first by rewrite lookup_insert.
+    iDestruct (gstacks_put_back with "Hfl HM") as "HM"; first by rewrite lookup_insert_eq.
     iSpecialize ("HWBWP" with "HM").
     iApply (clwp_wand with "[$]").
     iIntros (?); iDestruct 1 as (N) "(%&HM&?)".
@@ -179,13 +179,13 @@ Section wp.
     { apply set_eq; intros p; split; [|set_solver]. destruct (decide (m = p)); set_solver. }
     iDestruct (gstacks_out_swap _ _ m s' with "HM") as "HM"; first done.
     assert (N !! m = Some s).
-    { eapply lookup_weaken; last eassumption. rewrite lookup_insert //. }
+    { eapply lookup_weaken; last eassumption. rewrite lookup_insert_eq //. }
     simplify_eq /=.
     iExists _; iFrame.
     iPureIntro.
     apply map_subseteq_spec.
     intros i ? HMi.
-    destruct (decide (i = m)) as [->|]; first by rewrite HMns' in HMi; rewrite lookup_insert.
+    destruct (decide (i = m)) as [->|]; first by rewrite HMns' in HMi; rewrite lookup_insert_eq.
     rewrite lookup_insert_ne //.
     eapply lookup_weaken; last eassumption.
     rewrite lookup_insert_ne //.
@@ -205,11 +205,11 @@ Section wp.
     iMod (gstack_alloc with "HM") as (m) "(%&HM&Hfr)".
     iDestruct (gstack_frag_exists with "Hfr") as "#Hex".
     iDestruct (gstacks_take_out with "Hex HM") as (s Hs) "[HM Hfl]"; first set_solver.
-    rewrite lookup_insert in Hs; simplify_eq.
+    rewrite lookup_insert_eq in Hs; simplify_eq.
     iMod ("Hstk" with "[] Hfl Hfr") as (s) "[Hfl HR]"; first set_solver.
     iDestruct (gstacks_out_swap _ _ m s with "HM") as "HM"; first set_solver.
-    iPoseProof (gstacks_put_back with "Hfl HM") as "HM"; first by rewrite lookup_insert.
-    rewrite insert_insert.
+    iPoseProof (gstacks_put_back with "Hfl HM") as "HM"; first by rewrite lookup_insert_eq.
+    rewrite insert_insert_eq.
     replace ((out ∪ {[m]}) ∖ {[m]}) with out by set_solver.
     iApply (clwp_wand with "[-]").
     { iApply ("HWP" with "[] [$] [$]"). set_solver. }