diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 902af482f9a935a53a3328530b80fda5495256b6..cb3d556bd0de0a85335e25d32eeed9a56336fa74 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -56,7 +56,7 @@ trigger-iris.dev:
   variables:
     STDPP_REPO: "iris/stdpp"
     IRIS_REPO: "iris/iris"
-    OPAM_PINS: "coq version 8.15.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version 8.16.dev   git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   except:
   only:
     refs:
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index a8df583211d3b4f0822538507ed79ef395f08bc3..5fc548e9d4aedd5c84faa8fa6c158e4e3a1f2db1 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -61,7 +61,7 @@ Section fixpoint.
       { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
       apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
       + apply bi.limit_preserving_Persistent; solve_proper.
-      + apply limit_preserving_impl, bi.limit_preserving_entails;
+      + apply limit_preserving_impl', bi.limit_preserving_entails;
         solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
 
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index f4325de40f28ea8ae809854b00e21c17c6d75355..3b0284d85112a3d84eee829d3f7f0d96cad95a77 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -209,7 +209,7 @@ Section typing.
     iDestruct (ty_size_eq with "Hrown") as ">Heq". iDestruct "Heq" as %Heq.
     (* FIXME: Changing the order of $Hr↦ $Hc'↦ breaks applying...?? *)
     wp_apply (wp_memcpy with "[$Hr↦ $Hc'↦]").
-    { by rewrite Heq. }
+    { rewrite Heq /= ?Nat2Z.id //. }
     { f_equal. done. }
     iIntros "[Hr↦ Hc'↦]". wp_seq.
     iDestruct "Hx" as "[Hx↦ Hx†]". iDestruct "Hx↦" as (vx) "[Hx↦ Hxown]".
@@ -225,7 +225,7 @@ Section typing.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
       iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
       - iFrame. iExists _. iFrame. iNext. iApply uninit_own. done.
-      - iFrame. iExists _. iFrame. }
+      - try rewrite !Nat2Z.id. iFrame. iExists _. iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.