diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index edbd371f5bea8532b809419ff93713208c996c11..b5d1f3e6027bdf8feff3af54d91b1c74f91110b7 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2022-11-30.1.e52255ba") | (= "dev") }
+  "coq-iris" { (= "dev.2023-03-07.1.7e127436") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 5fc548e9d4aedd5c84faa8fa6c158e4e3a1f2db1..b78bed962707a021a23c341d959a8e6985265693 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -12,7 +12,7 @@ Section fixpoint_def.
   Local Instance type_2_contractive : Contractive (Nat.iter 2 T).
   Proof using Type*.
     intros n ? **. simpl.
-    by apply dist_later_dist, type_dist2_dist_later, HT, HT, type_later_dist2_later.
+    by apply dist_later_S, type_dist2_dist_later, HT, HT, type_later_dist2_later.
   Qed.
 
   Definition type_fixpoint : type := fixpointK 2 T.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 71e325141667c1511e4040c951922f2eda12cdb6..9ff32f797cc42e0a7ce6470d60905f0c0ba5464f 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -76,12 +76,12 @@ Section fn.
     Proper (pointwise_relation A (fn_params_rel (type_dist2_later n')) ==>
             type_dist2 n') fn.
   Proof.
-    intros fp1 fp2 Hfp. apply ty_of_st_type_ne. destruct n'; first done.
+    intros fp1 fp2 Hfp. apply ty_of_st_type_ne. dist_later_fin_intro.
     constructor; unfold ty_own; simpl.
     (* TODO: 'f_equiv' is slow here because reflexivity is slow. *)
     (* The clean way to do this would be to have a metric on type contexts. Oh well. *)
     intros tid vl. unfold typed_body.
-    do 12 f_equiv. f_contractive.
+    do 12 f_equiv. f_contractive_fin.
     do 18 ((eapply fp_E_proper; try reflexivity) || exact: Hfp || f_equiv).
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
       rewrite !tctx_interp_singleton /tctx_elt_interp /=.
@@ -94,7 +94,7 @@ Section fn.
             end)%I).
       { intros Hprop. apply Hprop, list_fmap_ne; last first.
         - symmetry. eapply Forall2_impl; first apply Hfp. intros.
-          apply dist_later_dist, type_dist2_dist_later. done.
+          apply dist_later_S, type_dist2_dist_later. done.
         - solve_proper. }
       clear. intros n tid p i x y. rewrite list_dist_lookup=>/(_ i).
       case _ : (x !! i)=>[tyx|]; case  _ : (y !! i)=>[tyy|];
@@ -104,7 +104,7 @@ Section fn.
   Global Instance fn_ne n' :
     Proper (pointwise_relation A (fn_params_rel (dist n')) ==> dist n') fn.
   Proof.
-    intros ?? Hfp. apply dist_later_dist, type_dist2_dist_later.
+    intros ?? Hfp. apply dist_later_S, type_dist2_dist_later.
     apply fn_type_contractive=>u. split; last split.
     - eapply Forall2_impl; first apply Hfp. intros. simpl.
       apply type_dist_dist2. done.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index cf2cf6c93e4bfd2e9be2360539a3957b7f96cd09..2339ac8d6b8e676491c2895500615f8b97ca39eb 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -34,7 +34,7 @@ Section arc.
   Proof.
     unfold arc_persist, P1, P2.
     solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                     f_type_equiv || f_contractive || f_equiv).
+                                     f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Lemma arc_persist_type_incl tid ν γ l ty1 ty2:
@@ -167,7 +167,7 @@ Section arc.
   Proof.
     constructor=>/=; unfold arc, full_arc_own, shared_arc_own;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                       f_type_equiv || f_contractive || f_equiv).
+                                       f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance arc_ne : NonExpansive arc.
@@ -280,7 +280,7 @@ Section arc.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                       f_type_equiv || f_contractive || f_equiv).
+                                       f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance weak_ne : NonExpansive weak.
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index 79915e492c27d50f20e7a5f7a97852dad51342d2..d5ea827998618bc23e8540f19c8b0036eb851c81 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -227,7 +227,7 @@ Section ghostcell.
     Proper (type_dist2 n ==> dist n) (ghostcell_inv tid l β α).
   Proof.
     solve_proper_core
-      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance ghostcell_inv_ne tid l β α : NonExpansive (ghostcell_inv tid l β α).
@@ -329,7 +329,7 @@ Section ghostcell.
       solve_proper_core ltac:(
         fun _ => exact: type_dist2_S || (eapply ghostcell_inv_type_ne; try reflexivity) ||
                         (eapply ghostcell_inv_proj_type_ne; try reflexivity) ||
-                                              f_type_equiv || f_contractive || f_equiv).
+                                              f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance ghostcell_ne α : NonExpansive (ghostcell α).
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 29ac59019e843d94168767e479c5f1f020fa6214..4860947f3e0d9c8a4ffe48e605b11ad867815ffb 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -79,7 +79,7 @@ Section mutex.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S ||
-                                              f_type_equiv || f_contractive || f_equiv).
+                                              f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance mutex_ne : NonExpansive mutex.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index dc3ebf956948be3027f83bfe3719fd8320771f92..d793b11df01da9a120da7831e8697ce754729149 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -78,7 +78,7 @@ Section mguard.
   Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv
+      solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive_fin || f_equiv
                                     || exact: type_dist2_S).
   Qed.
   Global Instance mutexguard_ne α : NonExpansive (mutexguard α).
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 7806b1cbf5b28d1a8b472834867a9183acf24e16..6a397b3dba760b23e2f2b66f2f2f5b7e310258c9 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -74,7 +74,7 @@ Section rc.
   Global Instance rc_inv_ne tid ν γ l n :
     Proper (type_dist2 n ==> dist n) (rc_inv tid ν γ l).
   Proof.
-    solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv).
+    solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Definition rc_persist tid ν (γ : gname) (l : loc) (ty : type) : iProp Σ :=
@@ -93,7 +93,7 @@ Section rc.
     Proper (type_dist2 n ==> dist n) (rc_persist tid ν γ l).
   Proof.
     solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                     f_type_equiv || f_contractive || f_equiv).
+                                     f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Lemma rc_persist_type_incl tid ν γ l ty1 ty2:
@@ -200,7 +200,7 @@ Section rc.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                       f_type_equiv || f_contractive || f_equiv).
+                                       f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance rc_ne : NonExpansive rc.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index b2c016601c6077f32a46429a1d35f0bcf320f802..2680ceac51701339888786c61c2cf3683cf2668d 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -71,7 +71,7 @@ Section weak.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
-                                       f_type_equiv || f_contractive || f_equiv).
+                                       f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance weak_ne : NonExpansive weak.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index e90117a73bc96f06a091d857a74a5b6929b4b124..da4ced23933c370df1eee8c352e404d473c003b0 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -59,7 +59,7 @@ Section refcell_inv.
     Proper (type_dist2 n ==> dist n) (refcell_inv tid l γ α).
   Proof.
     solve_proper_core
-      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance refcell_inv_ne tid l γ α : NonExpansive (refcell_inv tid l γ α).
@@ -173,7 +173,7 @@ Section refcell.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply refcell_inv_type_ne; try reflexivity) ||
-                                              f_type_equiv || f_contractive || f_equiv).
+                                              f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance refcell_ne : NonExpansive refcell.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index f0fc7f51a83349e7e2a45b87135b197d7fc6e57d..ec3810b17fef648cb38e4d91944f7d66a80a5a55 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -51,7 +51,7 @@ Section rwlock_inv.
     Proper (type_dist2 n ==> dist n) (rwlock_inv tid_own tid_shr l γ α).
   Proof.
     solve_proper_core
-      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+      ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance rwlock_inv_ne tid_own tid_shr l γ α :
@@ -178,7 +178,7 @@ Section rwlock.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_type_ne; try reflexivity) ||
-                                              f_type_equiv || f_contractive || f_equiv).
+                                              f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
 
   Global Instance rwlock_ne : NonExpansive rwlock.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 063a273b85f75c6df755e694b9d4aaa9aadbfb07..8923840039a4f7828215ee42b061101d85bf3742 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -69,7 +69,7 @@ Section rwlockreadguard.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_type_ne; try reflexivity) ||
-                                              f_type_equiv || f_contractive || f_equiv).
+                                              f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
   Global Instance rwlockreadguard_ne α : NonExpansive (rwlockreadguard α).
   Proof. apply type_contractive_ne, _. Qed.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 801c4ab544312d994e28e20b9c90cb7295e65daa..61056b6df44afa9c688cca10a1cc43efaa74b83c 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -69,7 +69,7 @@ Section rwlockwriteguard.
   Proof.
     constructor;
       solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_type_ne; try reflexivity) ||
-                                              f_type_equiv || f_contractive || f_equiv).
+                                              f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
   Global Instance rwlockwriteguard_ne α : NonExpansive (rwlockwriteguard α).
   Proof. apply type_contractive_ne, _. Qed.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 64e558d42fb8dde34ad7aa4d7fdd33974f4eee7b..3a2606b530b8aa78451f12444d8aaefc95e67d1c 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -52,7 +52,7 @@ Section join_handle.
   Global Instance join_handle_type_contractive : TypeContractive join_handle.
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => progress unfold join_inv || exact: type_dist2_dist || f_type_equiv || f_contractive || f_equiv).
+      solve_proper_core ltac:(fun _ => progress unfold join_inv || exact: type_dist2_dist || f_type_equiv || f_contractive_fin || f_equiv).
   Qed.
   Global Instance join_handle_ne : NonExpansive join_handle.
   Proof. apply type_contractive_ne, _. Qed.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 7d7a8967574b8583fc6e96d2a9f8ae4d9b1f344c..1af5b44bdf7eb1b6e5c035f7c3493c3276609390 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -46,7 +46,7 @@ Section shr_bor.
 
   Global Instance shr_type_contractive κ : TypeContractive (shr_bor κ).
   Proof.
-    intros n ???. apply: ty_of_st_type_ne. destruct n; first done.
+    intros n ???. apply: ty_of_st_type_ne. dist_later_fin_intro.
     solve_type_proper.
   Qed.
 
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 7ab3a880bf9c7487e09098a4adc37ebd0a305812..c719d6f7deb14a7592c610bb4855435985ac3b1e 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -99,7 +99,7 @@ Section sum.
     { clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
     constructor; simpl.
     - by rewrite EQmax.
-    - intros tid vl. destruct n as [|n]=> //=. rewrite /ty_own /= EQmax.
+    - intros tid vl. dist_later_fin_intro. rewrite /ty_own /= EQmax.
       solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
     - intros κ tid l. unfold is_pad. rewrite EQmax.
       solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 66e82981f72c1e6e71e1661d6df1fc947eb3b8ae..e577ecff2e8f8ba062e73fe07ed6bdf746f26b9d 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -295,13 +295,14 @@ Section type_dist2.
   Proof. intros EQ. split; intros; try apply dist_dist_later; apply EQ. Qed.
   Lemma type_dist2_dist_later n ty1 ty2 : type_dist2 n ty1 ty2 → dist_later n ty1 ty2.
   Proof.
-    intros EQ. destruct n; first done. split; intros; try apply EQ.
+    intros EQ. eapply dist_later_fin_iff. destruct n; first done.
+    split; intros; try apply EQ; try si_solver.
     apply dist_S, EQ.
   Qed.
   Lemma type_later_dist2_later n ty1 ty2 : dist_later n ty1 ty2 → type_dist2_later n ty1 ty2.
-  Proof. destruct n; first done. exact: type_dist_dist2. Qed.
+  Proof. destruct n; first done. rewrite dist_later_fin_iff. exact: type_dist_dist2. Qed.
   Lemma type_dist2_dist n ty1 ty2 : type_dist2 (S n) ty1 ty2 → dist n ty1 ty2.
-  Proof. move=>/type_dist2_dist_later. done. Qed.
+  Proof. move=>/type_dist2_dist_later. rewrite dist_later_fin_iff. done. Qed.
   Lemma type_dist2_S n ty1 ty2 : type_dist2 (S n) ty1 ty2 → type_dist2 n ty1 ty2.
   Proof. intros. apply type_dist_dist2, type_dist2_dist. done. Qed.
 
@@ -309,7 +310,7 @@ Section type_dist2.
   Proof. intros ?? EQ. apply EQ. Qed.
   Lemma ty_own_type_dist n:
     Proper (type_dist2 (S n) ==> eq ==> eq ==> dist n) ty_own.
-  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+  Proof. intros ?? EQ ??-> ??->. apply EQ. si_solver. Qed.
   Lemma ty_shr_type_dist n :
     Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
   Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
@@ -352,22 +353,22 @@ Section type_contractive.
   Lemma type_contractive_type_ne T :
     TypeContractive T → TypeNonExpansive T.
   Proof.
-    intros HT ? ???. apply type_dist_dist2, dist_later_dist, type_dist2_dist_later, HT. done.
+    intros HT ? ???. eapply type_dist_dist2, dist_later_S, type_dist2_dist_later, HT. done.
   Qed.
 
   Lemma type_contractive_ne T :
     TypeContractive T → NonExpansive T.
   Proof.
-    intros HT ? ???. apply dist_later_dist, type_dist2_dist_later, HT, type_dist_dist2. done.
+    intros HT ? ???. apply dist_later_S, type_dist2_dist_later, HT, type_dist_dist2. done.
   Qed.
 
   (* Simple types *)
   Global Instance ty_of_st_type_ne n :
     Proper (dist_later n ==> type_dist2 n) ty_of_st.
   Proof.
-    intros ???. constructor.
+    intros ?? Hdst. constructor.
     - done.
-    - intros. destruct n; first done; simpl. f_equiv. done.
+    - intros. dist_later_intro. eapply Hdst.
     - intros. solve_contractive.
   Qed.
 End type_contractive.
@@ -376,11 +377,11 @@ End type_contractive.
 Ltac f_type_equiv :=
   first [ ((eapply ty_size_type_dist || eapply ty_shr_type_dist || eapply ty_own_type_dist); try reflexivity) |
           match goal with | |- @dist_later ?A _ ?n ?x ?y =>
-                            destruct n as [|n]; [exact I|change (@dist A _ n x y)]
+                            eapply dist_later_fin_iff; destruct n as [|n]; [exact I|change (@dist A _ n x y)]
           end ].
 Ltac solve_type_proper :=
   constructor;
-  solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv).
+  solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive_fin || f_equiv).
 
 
 Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=