diff --git a/opam.pins b/opam.pins
index b496f750fc3ef03c16bcba873827a7483400ccee..eac978961c9f0d61cf9020abe751911b92b0691b 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 02bc52b4d905eb635940ff8545d59676ad44ea8c
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 15be3526bf8e9cff9a8cf7b97973367e0f697b6e
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 9731f5be58e56a14c2b01e34a75978bf6179e8d6..2ac03c240b9d194dcd7ff6d26ea946cbfd1fadce 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -33,8 +33,7 @@ Section fn.
     intros tid vl. destruct n' as [|n']; simpl; [done|]. unfold typed_body.
     do 12 f_equiv. f_contractive. do 17 f_equiv.
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
-      rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat f_equiv. apply Hty.
-      by rewrite (ty_size_ne _ _ _ (Hty _)).
+      rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat (apply Hty || f_equiv).
     - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
       cut (∀ n tid p i, Proper (dist (S n) ==> dist n)
         (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).