diff --git a/opam.pins b/opam.pins
index eac978961c9f0d61cf9020abe751911b92b0691b..63a5acc47dd361597b7b33e3e4fb47d9f6c91772 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 15be3526bf8e9cff9a8cf7b97973367e0f697b6e
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 6456f1f92fa1fc40b823535dedd8b3989827fd06
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index a248f6d5c1dff2e8f2b67fb9a0b7fffa0199152a..bfe1304145495e02fec2d60814e00c865db71049 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -1,63 +1,73 @@
 From lrust.lang Require Import proofmode.
 From lrust.typing Require Export lft_contexts type bool.
 Set Default Proof Using "Type".
+Import uPred.
 
-Section fixpoint.
+Section fixpoint_def.
   Context `{typeG Σ}.
+  Context (T : type → type) {HT: TypeContractive T}.
 
   Global Instance type_inhabited : Inhabited type := populate bool.
+  
+  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.
+  Qed.
+
+  Definition type_fixpoint : type := fixpointK 2 T.
+End fixpoint_def.
 
-  Context (T : type → type) `{Contractive T}.
+Section fixpoint.
+  Context `{typeG Σ}.
+  Context (T : type → type) {HT: TypeContractive T}.
 
   Global Instance fixpoint_copy :
-    (∀ `(!Copy ty), Copy (T ty)) → Copy (fixpoint T).
+    (∀ `(!Copy ty), Copy (T ty)) → Copy (type_fixpoint T).
   Proof.
-    intros ?. apply fixpoint_ind.
-    - intros ??[EQsz%leibniz_equiv EQown EQshr].
-      specialize (λ tid vl, EQown tid vl). specialize (λ κ tid l, EQshr κ tid l).
-      simpl in *=>-[Hp Hsh]; (split; [intros ??|intros ???]).
-      + revert Hp. by rewrite /PersistentP -EQown.
-      + intros F l q. rewrite -EQsz -EQshr. setoid_rewrite <-EQown. auto.
+    intros ?. unfold type_fixpoint. apply fixpointK_ind.
+    - apply type_contractive_ne, _.
+    - apply copy_equiv.
     - exists bool. apply _.
     - done.
-    - intros c Hc. split.
-      + intros tid vl. apply uPred.equiv_entails, equiv_dist=>n.
-        by rewrite conv_compl uPred.always_always.
-      + intros κ tid E F l q ? ?.
-        apply uPred.entails_equiv_and, equiv_dist=>n. etrans.
-        { apply equiv_dist, uPred.entails_equiv_and, (copy_shr_acc κ tid E F)=>//.
-            by rewrite -conv_compl. }
-        symmetry.
-        do 2 f_equiv; first by rewrite conv_compl. set (cn:=c n).
-        repeat (apply (conv_compl n c) || f_contractive || f_equiv);
-          by rewrite conv_compl. (* slow, FIXME *)
+    - (* If Copy was an Iris assertion, this would be trivial -- we'd just
+         use entails_lim once.  However, on the Coq side, it is more convenient
+         as a record -- so this is where we pay. *)
+      intros c Hc. split.
+      + intros tid vl. rewrite /PersistentP. entails_lim c; [solve_proper..|].
+        intros. apply (Hc n).
+      + intros κ tid E F l q ? ?. entails_lim c; first solve_proper.
+        * solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
+        * intros n. apply (Hc n); first done. erewrite ty_size_ne; first done.
+          rewrite conv_compl. done.
   Qed.
 
   Global Instance fixpoint_send :
-    (∀ `(!Send ty), Send (T ty)) → Send (fixpoint T).
+    (∀ `(!Send ty), Send (T ty)) → Send (type_fixpoint T).
   Proof.
-    intros ?. apply fixpoint_ind.
-    - intros ?? EQ ????. by rewrite -EQ.
+    intros ?. unfold type_fixpoint. apply fixpointK_ind.
+    - apply type_contractive_ne, _.
+    - apply send_equiv.
     - exists bool. apply _.
     - done.
-    - intros c Hc ???. apply uPred.entails_equiv_and, equiv_dist=>n.
-      rewrite conv_compl. apply equiv_dist, uPred.entails_equiv_and; apply Hc.
+    - intros c Hc ???. entails_lim c; [solve_proper..|]. intros n. apply Hc.
   Qed.
 
   Global Instance fixpoint_sync :
-    (∀ `(!Sync ty), Sync (T ty)) → Sync (fixpoint T).
+    (∀ `(!Sync ty), Sync (T ty)) → Sync (type_fixpoint T).
   Proof.
-    intros ?. apply fixpoint_ind.
-    - intros ?? EQ ?????. by rewrite -EQ.
+    intros ?. unfold type_fixpoint. apply fixpointK_ind.
+    - apply type_contractive_ne, _.
+    - apply sync_equiv.
     - exists bool. apply _.
     - done.
-    - intros c Hc ????. apply uPred.entails_equiv_and, equiv_dist=>n.
-      rewrite conv_compl. apply equiv_dist, uPred.entails_equiv_and; apply Hc.
+    - intros c Hc ????. entails_lim c; [solve_proper..|]. intros n. apply Hc.
   Qed.
 
-  Lemma fixpoint_unfold_eqtype E L : eqtype E L (fixpoint T) (T (fixpoint T)).
+  Lemma fixpoint_unfold_eqtype E L : eqtype E L (type_fixpoint T) (T (type_fixpoint T)).
   Proof.
-    unfold eqtype, subtype, type_incl. setoid_rewrite <-fixpoint_unfold.
+    unfold eqtype, subtype, type_incl.
+    setoid_rewrite <-fixpointK_unfold; [| by apply type_contractive_ne, _..].
     split; iIntros "_ _"; (iSplit; first done); iSplit; iIntros "!#*$".
   Qed.
 End fixpoint.
@@ -66,87 +76,44 @@ Section subtyping.
   Context `{typeG Σ} (E : elctx) (L : llctx).
 
   (* TODO : is there a way to declare these as a [Proper] instances ? *)
-  Lemma fixpoint_mono T1 `{Contractive T1} T2 `{Contractive T2} :
+  Lemma fixpoint_mono T1 `{!TypeContractive T1} T2 `{!TypeContractive T2} :
     (∀ ty1 ty2, subtype E L ty1 ty2 → subtype E L (T1 ty1) (T2 ty2)) →
-    subtype E L (fixpoint T1) (fixpoint T2).
+    subtype E L (type_fixpoint T1) (type_fixpoint T2).
   Proof.
-    intros H12. apply fixpoint_ind.
+    intros H12. rewrite /type_fixpoint. apply fixpointK_ind.
+    - apply type_contractive_ne, _.
     - intros ?? EQ ?. etrans; last done. by apply equiv_subtype.
     - by eexists _.
-    - intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
-    - intros c Hc.
-      assert (Hsz : lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                ⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)⌝).
-      { iIntros "HE HL". rewrite (conv_compl 0 c) /=.
-        iDestruct (Hc 0%nat with "HE HL") as "[$ _]". }
-      assert (Hown : lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ tid vl, (compl c).(ty_own) tid vl -∗ (fixpoint T2).(ty_own) tid vl)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl (S n) c) as [_ Heq _]; simpl in *. setoid_rewrite Heq.
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "HE HL".
-        iDestruct (Hc (S n) with "HE HL") as "[_ [$ _]]". }
-      assert (Hshr : lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ κ tid l,
-                   (compl c).(ty_shr) κ tid l -∗ (fixpoint T2).(ty_shr) κ tid l)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl n c) as [_ _ Heq]; simpl in *. setoid_rewrite Heq.
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "HE HL".
-        iDestruct (Hc n with "HE HL") as "[_ [_ $]]". }
-      iIntros "HE HL". iSplit; [|iSplit].
-      + iApply (Hsz with "HE HL").
-      + iApply (Hown with "HE HL").
-      + iApply (Hshr with "HE HL").
+    - intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12.
+    - intros c Hc. rewrite /subtype. entails_lim c; [solve_proper..|].
+      intros n. apply Hc.
   Qed.
 
-  Lemma fixpoint_proper T1 `{Contractive T1} T2 `{Contractive T2} :
+  Lemma fixpoint_proper T1 `{TypeContractive T1} T2 `{TypeContractive T2} :
     (∀ ty1 ty2, eqtype E L ty1 ty2 → eqtype E L (T1 ty1) (T2 ty2)) →
-    eqtype E L (fixpoint T1) (fixpoint T2).
+    eqtype E L (type_fixpoint T1) (type_fixpoint T2).
   Proof.
-    intros H12. apply fixpoint_ind.
+    intros H12. rewrite /type_fixpoint. apply fixpointK_ind.
+    - apply type_contractive_ne, _.
     - intros ?? EQ ?. etrans; last done. by apply equiv_eqtype.
     - by eexists _.
-    - intros. rewrite (fixpoint_unfold_eqtype T2). by apply H12.
-    - intros c Hc. setoid_rewrite eqtype_unfold in Hc. rewrite eqtype_unfold.
-      assert (Hsz : lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                ⌜(compl c).(ty_size) = (fixpoint T2).(ty_size)⌝).
-      { iIntros "HE HL". rewrite (conv_compl 0 c) /=.
-        iDestruct (Hc 0%nat with "HE HL") as "[$ _]". }
-      assert (Hown : lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ tid vl, (compl c).(ty_own) tid vl ↔ (fixpoint T2).(ty_own) tid vl)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl (S n) c) as [_ Heq _]; simpl in *. setoid_rewrite Heq.
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "HE HL".
-        iDestruct (Hc (S n) with "HE HL") as "[_ [$ _]]". }
-      assert (Hshr : lft_contexts.elctx_interp_0 E -∗
-                ⌜lft_contexts.llctx_interp_0 L⌝ -∗
-                □ (∀ κ tid l,
-                   (compl c).(ty_shr) κ tid l ↔ (fixpoint T2).(ty_shr) κ tid l)).
-      { apply uPred.entails_equiv_and, equiv_dist=>n.
-        destruct (conv_compl n c) as [_ _ Heq]. setoid_rewrite Heq.
-        apply equiv_dist, uPred.entails_equiv_and. iIntros "HE HL".
-        iDestruct (Hc n with "HE HL") as "[_ [_ $]]". }
-      iIntros "HE HL". iSplit; [|iSplit].
-      + iApply (Hsz with "HE HL").
-      + iApply (Hown with "HE HL").
-      + iApply (Hshr with "HE HL").
+    - intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12.
+    - intros c Hc. split; rewrite /subtype; (entails_lim c; [solve_proper..|]);
+      intros n; apply Hc.
   Qed.
 
-  Lemma fixpoint_unfold_subtype_l ty T `{Contractive T} :
-    subtype E L ty (T (fixpoint T)) → subtype E L ty (fixpoint T).
+  (* FIXME: Some rewrites here are slower than one would expect. *)
+  Lemma fixpoint_unfold_subtype_l ty T `{TypeContractive T} :
+    subtype E L ty (T (type_fixpoint T)) → subtype E L ty (type_fixpoint T).
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_subtype_r ty T `{Contractive T} :
-    subtype E L (T (fixpoint T)) ty → subtype E L (fixpoint T) ty.
+  Lemma fixpoint_unfold_subtype_r ty T `{TypeContractive T} :
+    subtype E L (T (type_fixpoint T)) ty → subtype E L (type_fixpoint T) ty.
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_eqtype_l ty T `{Contractive T} :
-    eqtype E L ty (T (fixpoint T)) → eqtype E L ty (fixpoint T).
+  Lemma fixpoint_unfold_eqtype_l ty T `{TypeContractive T} :
+    eqtype E L ty (T (type_fixpoint T)) → eqtype E L ty (type_fixpoint T).
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_eqtype_r ty T `{Contractive T} :
-    eqtype E L (T (fixpoint T)) ty → eqtype E L (fixpoint T) ty.
+  Lemma fixpoint_unfold_eqtype_r ty T `{TypeContractive T} :
+    eqtype E L (T (type_fixpoint T)) ty → eqtype E L (type_fixpoint T) ty.
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
 End subtyping.
 
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 2ac03c240b9d194dcd7ff6d26ea946cbfd1fadce..6786f64eda20e21c7a0f1bbe7f73f7a51e0525a6 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -25,20 +25,25 @@ Section fn.
   Global Instance fn_send E tys ty : Send (fn E tys ty).
   Proof. iIntros (tid1 tid2 vl). done. Qed.
 
-  Lemma fn_contractive n' E :
-    Proper (pointwise_relation A (dist_later n') ==>
-            pointwise_relation A (dist_later n') ==> dist n') (fn E).
+  Lemma fn_type_contractive n' E :
+    Proper (pointwise_relation A (B := vec type n) (Forall2 (type_dist2_later n')) ==>
+            pointwise_relation A (type_dist2_later n') ==> type_dist2 n') (fn E).
   Proof.
-    intros ?? Htys ?? Hty. apply ty_of_st_ne; constructor.
-    intros tid vl. destruct n' as [|n']; simpl; [done|]. unfold typed_body.
+    intros ?? Htys ?? Hty. apply ty_of_st_type_ne. destruct n'; first done.
+    constructor; 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 17 f_equiv.
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
       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)
+      cut (∀ n tid p i, Proper (dist n ==> dist n)
         (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).
-      { intros Hprop. apply Hprop, list_fmap_ne, Htys. intros ty1 ty2 Hty12.
-        rewrite (ty_size_ne _ _ _ Hty12). by rewrite Hty12. }
+      { intros Hprop. apply Hprop, list_fmap_ne; last first.
+        - eapply Forall2_impl; first exact: Htys. intros.
+          apply dist_later_dist, type_dist2_dist_later. done.
+        - intros ty1 ty2 Hty12. rewrite (ty_size_ne _ _ _ Hty12). by rewrite Hty12. }
       clear. intros n tid p i x y. rewrite list_dist_lookup=>Hxy.
       specialize (Hxy i). destruct (x !! i) as [tyx|], (y !! i) as [tyy|];
         inversion_clear Hxy; last done.
@@ -52,15 +57,17 @@ Section fn.
         * iIntros "H". by iApply "H".
         * iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
   Qed.
-  Global Existing Instance fn_contractive.
+  Global Existing Instance fn_type_contractive.
 
   Global Instance fn_ne n' E :
     Proper (pointwise_relation A (dist n') ==>
             pointwise_relation A (dist n') ==> dist n') (fn E).
   Proof.
-    intros ?? H1 ?? H2.
-    apply fn_contractive=>u; (destruct n'; [done|apply dist_S]);
-      [apply (H1 u)|apply (H2 u)].
+    intros ?? H1 ?? H2. apply dist_later_dist, type_dist2_dist_later.
+    apply fn_type_contractive=>u; simpl.
+    - eapply Forall2_impl; first exact: H1. intros. simpl.
+      apply type_dist_dist2. done.
+    - apply type_dist_dist2. apply H2.
   Qed.
 End fn.
 
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 42a811c8841819345de222fcccb9cb08cdfa6b7d..25eba634ea8fad570bf9ac2019548fc6bd75a123 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -129,15 +129,11 @@ Section own.
     eqtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
   Proof. intros. by apply own_proper. Qed.
 
-  Global Instance own_contractive n : Contractive (own_ptr n).
-  Proof.
-    intros m ?? EQ. constructor; simpl.
-    - done.
-    - destruct m=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
-    - intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
-  Qed.
-  Global Instance own_ne n m : Proper (dist m ==> dist m) (own_ptr n).
-  Proof. apply contractive_ne, _. Qed.
+  Global Instance own_type_contractive n : TypeContractive (own_ptr n).
+  Proof. solve_type_proper. Qed.
+
+  Global Instance own_ne n : NonExpansive (own_ptr n).
+  Proof. apply type_contractive_ne, _. Qed.
 
   Global Instance own_send n ty :
     Send ty → Send (own_ptr n ty).
@@ -157,6 +153,7 @@ Section own.
   Qed.
 End own.
 
+(* TODO: Make box a proper type with subtyping, contractivity, ... *)
 Notation box ty := (own_ptr ty.(ty_size) ty).
 
 Section typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 6e7d11215165dbb721d740f8b6770a34c975f9e0..86916b7e57b38da8ccfd11d31fa594d7fa750d56 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -67,14 +67,9 @@ Section product.
     iSplitL "H1"; by iApply (ty_shr_mono with "H⊑").
   Qed.
 
-  Global Instance product2_ne n:
-    Proper (dist n ==> dist n ==> dist n) product2.
-  Proof.
-    intros ?? EQ1 ?? EQ2. constructor; simpl.
-    - by rewrite EQ1 EQ2.
-    - intros tid vs. destruct n as [|n]=>//=. by setoid_rewrite EQ1; setoid_rewrite EQ2.
-    - intros ???. by rewrite EQ1 EQ2. (* slow, FIXME *)
-  Qed.
+  Global Instance product2_type_ne n:
+    Proper (type_dist2 n ==> type_dist2 n ==> type_dist2 n) product2.
+  Proof. solve_type_proper. Qed.
 
   Global Instance product2_mono E L:
     Proper (subtype E L ==> subtype E L ==> subtype E L) product2.
@@ -144,7 +139,7 @@ Section product.
   Definition product := foldr product2 unit0.
   Definition unit := product [].
 
-  Global Instance product_ne n: Proper (dist n ==> dist n) product.
+  Global Instance product_type_ne n: Proper (Forall2 (type_dist2 n) ==> type_dist2 n) product.
   Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
   Global Instance product_mono E L:
     Proper (Forall2 (subtype E L) ==> subtype E L) product.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 87e26d67154483b2c69b8fe5b6b7da8d7c2b2af0..678aeb85dbddceeb66eab7eff5b04920c07ad68e 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -32,13 +32,14 @@ Section shr_bor.
     Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) shr_bor.
   Proof. intros ??[] ??[]. by split; apply shr_mono. Qed.
 
-  Global Instance shr_contractive κ : Contractive (shr_bor κ).
+  Global Instance shr_type_contractive κ : TypeContractive (shr_bor κ).
   Proof.
-    intros n ?? EQ. apply ty_of_st_ne; constructor=> //=.
-    intros tid vl. destruct n as [n|]=>//=. repeat f_equiv. apply EQ.
+    intros n ???. apply: ty_of_st_type_ne. destruct n; first done.
+    solve_type_proper.
   Qed.
-  Global Instance shr_ne κ n : Proper (dist n ==> dist n) (shr_bor κ).
-  Proof. apply contractive_ne, _. Qed.
+
+  Global Instance shr_ne κ : NonExpansive (shr_bor κ).
+  Proof. apply type_contractive_ne, _. Qed.
 
   Global Instance shr_send κ ty :
     Sync ty → Send (shr_bor κ ty).
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index dd77079db48beec264d7e7253f4e4cb1a5326692..0d598a27de6b3e71e486658100814f5408c3f534 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -95,21 +95,22 @@ Section sum.
     - iApply ((nth i tyl ∅).(ty_shr_mono) with "Hord"); done.
   Qed.
 
-  Global Instance sum_ne n: Proper (dist n ==> dist n) sum.
+  Global Instance sum_type_ne n: Proper (Forall2 (type_dist2 n) ==> type_dist2 n) sum.
   Proof.
     intros x y EQ.
     assert (EQmax : list_max (map ty_size x) = list_max (map ty_size y)).
     { induction EQ as [|???? EQ _ IH]=>//=.
       rewrite IH. f_equiv. apply EQ. }
-    assert (EQnth :∀ i, nth i x ∅ ≡{n}≡ nth i y ∅).
+    (* TODO: If we had the right lemma relating nth, (Forall2 R) and R, we should
+       be able to make this more automatic. *)
+    assert (EQnth :∀ i, type_dist2 n (nth i x ∅) (nth i y ∅)).
     { clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
     constructor; simpl.
     - by rewrite EQmax.
-    - intros tid vl. destruct n as [|n]=> //=. rewrite EQmax. by setoid_rewrite EQnth.
+    - intros tid vl. destruct n as [|n]=> //=. rewrite EQmax.
+      solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
     - intros κ tid l. unfold is_pad. rewrite EQmax.
-      assert (EQsz : ∀ i, (nth i x ∅).(ty_size) = (nth i y ∅).(ty_size))
-        by (intros; apply EQnth).
-      repeat (rewrite EQsz || apply EQnth || f_equiv).
+      solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
   Qed.
 
   Global Instance sum_mono E L :
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1f69cae8a9700745fecf0eafa9fa6a7438403c1c..c9eb29858752dcb2f4fec7498ebb253ac2126d71 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -57,144 +57,30 @@ Record simple_type `{typeG Σ} :=
 Existing Instance st_own_persistent.
 Instance: Params (@st_own) 2.
 
-Section type.
-  Context `{typeG Σ}.
-
-  (** Copy types *)
-  Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
-    match n with
-    | 0%nat => ∅
-    | S n => ↑shrN.@l ∪ shr_locsE (shift_loc l 1%nat) n
-    end.
-
-  Lemma shr_locsE_shift l n m :
-    shr_locsE l (n + m) = shr_locsE l n ∪ shr_locsE (shift_loc l n) m.
-  Proof.
-    revert l; induction n; intros l.
-    - rewrite shift_loc_0. set_solver+.
-    - rewrite -Nat.add_1_l Nat2Z.inj_add /= IHn shift_loc_assoc.
-      set_solver+.
-  Qed.
-
-  Lemma shr_locsE_disj l n m :
-    shr_locsE l n ⊥ shr_locsE (shift_loc l n) m.
-  Proof.
-    revert l; induction n; intros l.
-    - simpl. set_solver+.
-    - rewrite -Nat.add_1_l Nat2Z.inj_add /=.
-      apply disjoint_union_l. split; last (rewrite -shift_loc_assoc; exact: IHn).
-      clear IHn. revert n; induction m; intros n; simpl; first set_solver+.
-      rewrite shift_loc_assoc. apply disjoint_union_r. split.
-      + apply ndot_ne_disjoint. destruct l. intros [=]. omega.
-      + rewrite -Z.add_assoc. move:(IHm (n + 1)%nat). rewrite Nat2Z.inj_add //.
-  Qed.
-
-  Lemma shr_locsE_shrN l n :
-    shr_locsE l n ⊆ ↑shrN.
-  Proof.
-    revert l; induction n=>l /=; first by set_solver+.
-    apply union_least; last by auto. solve_ndisj.
-  Qed.
-
-  Lemma shr_locsE_subseteq l n m :
-    (n ≤ m)%nat → shr_locsE l n ⊆ shr_locsE l m.
-  Proof.
-    induction 1; first done. etrans; first done.
-    rewrite -Nat.add_1_l [(_ + _)%nat]comm_L shr_locsE_shift. set_solver+.
-  Qed.
-
-  Lemma shr_locsE_split_tok l n m tid :
-    na_own tid (shr_locsE l (n + m)) ⊣⊢
-      na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (shift_loc l n) m).
-  Proof.
-    rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
-  Qed.
-
-  Class Copy (t : type) := {
-    copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
-    copy_shr_acc κ tid E F l q :
-      lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
-      lft_ctx -∗ t.(ty_shr) κ tid l -∗ na_own tid F -∗ q.[κ] ={E}=∗
-         ∃ q', na_own tid (F ∖ shr_locsE l t.(ty_size)) ∗
-           ▷(l ↦∗{q'}: t.(ty_own) tid) ∗
-        (na_own tid (F ∖ shr_locsE l t.(ty_size)) -∗ ▷l ↦∗{q'}: t.(ty_own) tid
-                                    ={E}=∗ na_own tid F ∗ q.[κ])
-  }.
-  Global Existing Instances copy_persistent.
-
-  Class LstCopy (tys : list type) := lst_copy : Forall Copy tys.
-  Global Instance lst_copy_nil : LstCopy [] := List.Forall_nil _.
-  Global Instance lst_copy_cons ty tys :
-    Copy ty → LstCopy tys → LstCopy (ty::tys) := List.Forall_cons _ _ _.
-
-  (** Send and Sync types *)
-  Class Send (t : type) :=
-    send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
-
-  Class LstSend (tys : list type) := lst_send : Forall Send tys.
-  Global Instance lst_send_nil : LstSend [] := List.Forall_nil _.
-  Global Instance lst_send_cons ty tys :
-    Send ty → LstSend tys → LstSend (ty::tys) := List.Forall_cons _ _ _.
-
-  Class Sync (t : type) :=
-    sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
-
-  Class LstSync (tys : list type) := lst_sync : Forall Sync tys.
-  Global Instance lst_sync_nil : LstSync [] := List.Forall_nil _.
-  Global Instance lst_sync_cons ty tys :
-    Sync ty → LstSync tys → LstSync (ty::tys) := List.Forall_cons _ _ _.
-
-  (** Simple types *)
-  Program Definition ty_of_st (st : simple_type) : type :=
-    {| ty_size := 1; ty_own := st.(st_own);
-
-       (* [st.(st_own) tid vl] needs to be outside of the fractured
-          borrow, otherwise I do not know how to prove the shr part of
-          [subtype_shr_mono]. *)
-       ty_shr := λ κ tid l,
-                 (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗
-                        â–· st.(st_own) tid vl)%I
-    |}.
-  Next Obligation. intros. apply st_size_eq. Qed.
-  Next Obligation.
-    iIntros (st E κ l tid ??) "#LFT Hmt Hκ".
-    iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
-    iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
-    iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]". set_solver.
-    - iFrame "Hκ".
-      iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
-    - iExFalso. by iApply (lft_tok_dead with "Hκ").
-  Qed.
-  Next Obligation.
-    intros st κ κ' tid l. iIntros "#Hord H".
-    iDestruct "H" as (vl) "[#Hf #Hown]".
-    iExists vl. iFrame "Hown". by iApply (frac_bor_shorten with "Hord").
-  Qed.
-
-  Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
-  Next Obligation.
-    iIntros (st κ tid E ? l q ? HF) "#LFT #Hshr Htok Hlft".
-    iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
-    iDestruct "Hshr" as (vl) "[Hf Hown]".
-    iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
-    iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]".
-    iSplitL "Hmt1"; first by auto with iFrame.
-    iIntros "Htok2 Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
-    iDestruct ("Htok" with "Htok2") as "$".
-    iAssert (▷ ⌜length vl = length vl'⌝)%I as ">%".
-    { iNext. iDestruct (st_size_eq with "Hown") as %->.
-      iDestruct (st_size_eq with "Hown'") as %->. done. }
-    iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
-    iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
-  Qed.
-
-  Global Instance ty_of_st_sync st :
-    Send (ty_of_st st) → Sync (ty_of_st st).
-  Proof.
-    iIntros (Hsend κ tid1 tid2 l). iDestruct 1 as (vl) "[Hm Hown]".
-    iExists vl. iFrame "Hm". iNext. by iApply Hsend.
-  Qed.
-End type.
+Program Definition ty_of_st `{typeG Σ} (st : simple_type) : type :=
+  {| ty_size := 1; ty_own := st.(st_own);
+     (* [st.(st_own) tid vl] needs to be outside of the fractured
+         borrow, otherwise I do not know how to prove the shr part of
+         [subtype_shr_mono]. *)
+     ty_shr := λ κ tid l,
+               (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗
+                                                 â–· st.(st_own) tid vl)%I
+  |}.
+Next Obligation. intros. apply st_size_eq. Qed.
+Next Obligation.
+  iIntros (?? st E κ l tid ??) "#LFT Hmt Hκ".
+  iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
+  iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
+  iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]". set_solver.
+  - iFrame "Hκ".
+    iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
+  - iExFalso. by iApply (lft_tok_dead with "Hκ").
+Qed.
+Next Obligation.
+  iIntros (?? st κ κ' tid l) "#Hord H".
+  iDestruct "H" as (vl) "[#Hf #Hown]".
+  iExists vl. iFrame "Hown". by iApply (frac_bor_shorten with "Hord").
+Qed.
 
 Coercion ty_of_st : simple_type >-> type.
 
@@ -215,26 +101,26 @@ Section ofe.
   Inductive type_dist' (n : nat) (ty1 ty2 : type) : Prop :=
     Type_dist :
       ty1.(ty_size) = ty2.(ty_size) →
-      (∀ tid vs, dist_later n (ty1.(ty_own) tid vs) (ty2.(ty_own) tid vs)) →
+      (∀ tid vs, ty1.(ty_own) tid vs ≡{n}≡ ty2.(ty_own) tid vs) →
       (∀ κ tid l, ty1.(ty_shr) κ tid l ≡{n}≡ ty2.(ty_shr) κ tid l) →
       type_dist' n ty1 ty2.
   Instance type_dist : Dist type := type_dist'.
 
   Let T := prodC
-    (prodC natC (thread_id -c> list val -c> laterC (iProp Σ)))
+    (prodC natC (thread_id -c> list val -c> iProp Σ))
     (lft -c> thread_id -c> loc -c> iProp Σ).
   Let P (x : T) : Prop :=
     (∀ κ tid l, PersistentP (x.2 κ tid l)) ∧
-    (∀ tid vl, (later_car (x.1.2 tid vl) : iProp Σ) -∗ ⌜length vl = x.1.1⌝) ∧
+    (∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1⌝) ∧
     (∀ E κ l tid q, lftE ⊆ E →
-      lft_ctx -∗ &{κ} (l ↦∗: λ vs, later_car (x.1.2 tid vs)) -∗
+      lft_ctx -∗ &{κ} (l ↦∗: λ vs, x.1.2 tid vs) -∗
       q.[κ] ={E}=∗ x.2 κ tid l ∗ q.[κ]) ∧
     (∀ κ κ' tid l, κ' ⊑ κ -∗ x.2 κ tid l -∗ x.2 κ' tid l).
 
   Definition type_unpack (ty : type) : T :=
-    (ty.(ty_size), λ tid vl, Next (ty.(ty_own) tid vl), ty.(ty_shr)).
+    (ty.(ty_size), λ tid vl, (ty.(ty_own) tid vl), ty.(ty_shr)).
   Program Definition type_pack (x : T) (H : P x) : type :=
-    {| ty_size := x.1.1; ty_own tid vl := later_car (x.1.2 tid vl); ty_shr := x.2 |}.
+    {| ty_size := x.1.1; ty_own tid vl := x.1.2 tid vl; ty_shr := x.2 |}.
   Solve Obligations with by intros [[??] ?] (?&?&?&?).
 
   Definition type_ofe_mixin : OfeMixin type.
@@ -250,7 +136,7 @@ Section ofe.
   Global Instance ty_size_proper : Proper ((≡) ==> eq) ty_size.
   Proof. intros ?? EQ. apply EQ. Qed.
   Global Instance ty_own_ne n:
-    Proper (dist (S n) ==> eq ==> eq ==> dist n) ty_own.
+    Proper (dist n ==> eq ==> eq ==> dist n) ty_own.
   Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
   Global Instance ty_own_proper : Proper ((≡) ==> eq ==> eq ==> (≡)) ty_own.
   Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
@@ -267,15 +153,15 @@ Section ofe.
     - split; [by destruct 1|by intros [[??] ?]; constructor].
     - by intros [].
     - intros ? c. rewrite /P /=. split_and!.
+      (* TODO: Can we do these proofs without effectively going into the model? *)
       + intros κ tid l. apply uPred.entails_equiv_and, equiv_dist=>n.
         setoid_rewrite conv_compl; simpl.
         apply equiv_dist, uPred.entails_equiv_and, ty_shr_persistent.
       + intros tid vl. apply uPred.entails_equiv_and, equiv_dist=>n.
-        rewrite !conv_compl /=.
+        repeat setoid_rewrite conv_compl at 1. simpl.
         apply equiv_dist, uPred.entails_equiv_and, ty_size_eq.
       + intros E κ l tid q ?. apply uPred.entails_equiv_and, equiv_dist=>n.
         setoid_rewrite conv_compl; simpl.
-        rewrite -(c.(chain_cauchy) n (S n)); last lia.
         by apply equiv_dist, uPred.entails_equiv_and, ty_share.
       + intros κ κ' tid l. apply uPred.entails_equiv_and, equiv_dist=>n.
         setoid_rewrite conv_compl; simpl.
@@ -289,12 +175,12 @@ Section ofe.
   Instance st_equiv : Equiv simple_type := st_equiv'.
   Inductive st_dist' (n : nat) (ty1 ty2 : simple_type) : Prop :=
     St_dist :
-      (∀ tid vs, dist_later n (ty1.(ty_own) tid vs) (ty2.(ty_own) tid vs)) →
+      (∀ tid vs, ty1.(ty_own) tid vs ≡{n}≡ (ty2.(ty_own) tid vs)) →
       st_dist' n ty1 ty2.
   Instance st_dist : Dist simple_type := st_dist'.
 
-  Definition st_unpack (ty : simple_type) : thread_id -c> list val -c> laterC (iProp Σ) :=
-    λ tid vl, Next (ty.(ty_own) tid vl).
+  Definition st_unpack (ty : simple_type) : thread_id -c> list val -c> iProp Σ :=
+    λ tid vl, ty.(ty_own) tid vl.
 
   Definition st_ofe_mixin : OfeMixin simple_type.
   Proof.
@@ -305,7 +191,7 @@ Section ofe.
   Canonical Structure stC : ofeT := OfeT simple_type st_ofe_mixin.
 
   Global Instance st_own_ne n :
-    Proper (dist (S n) ==> eq ==> eq ==> dist n) st_own.
+    Proper (dist n ==> eq ==> eq ==> dist n) st_own.
   Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
   Global Instance st_own_proper : Proper ((≡) ==> eq ==> eq ==> (≡)) st_own.
   Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
@@ -314,12 +200,271 @@ Section ofe.
   Proof.
     intros n ?? EQ. constructor. done. simpl.
     - intros tid l. apply EQ.
-    - simpl. intros; repeat (f_contractive || f_equiv). apply EQ.
+    - simpl. intros; repeat f_equiv. apply EQ.
   Qed.
   Global Instance ty_of_st_proper : Proper ((≡) ==> (≡)) ty_of_st.
   Proof. apply (ne_proper _). Qed.
 End ofe.
 
+(** Special metric for type-nonexpansive and Type-contractive functions. *)
+Section type_dist2.
+  Context `{typeG Σ}.
+
+  (* Size and shr are n-equal, but own is only n-1-equal.
+     We need this to express what shr has to satisfy on a Type-NE-function:
+     It may only depend contractively on own. *)
+  (* TODO: Find a better name for this metric. *)
+  Inductive type_dist2 (n : nat) (ty1 ty2 : type) : Prop :=
+    Type_dist2 :
+      ty1.(ty_size) = ty2.(ty_size) →
+      (∀ tid vs, dist_later n (ty1.(ty_own) tid vs) (ty2.(ty_own) tid vs)) →
+      (∀ κ tid l, ty1.(ty_shr) κ tid l ≡{n}≡ ty2.(ty_shr) κ tid l) →
+      type_dist2 n ty1 ty2.
+
+  Global Instance type_dist2_equivalence : Equivalence (type_dist2 n).
+  Proof.
+    constructor.
+    - by constructor.
+    - intros ?? Heq; constructor; symmetry; eapply Heq.
+    - intros ??? Heq1 Heq2; constructor; etrans; (eapply Heq1 || eapply Heq2).
+  Qed.
+
+  Definition type_dist2_later (n : nat) ty1 ty2 : Prop :=
+    match n with O => True | S n => type_dist2 n ty1 ty2 end.
+  Arguments type_dist2_later !_ _ _ /.
+
+  Global Instance type_dist2_later_equivalence n :
+    Equivalence (type_dist2_later n).
+  Proof. destruct n as [|n]. by split. apply type_dist2_equivalence. Qed.
+
+  (* The hierarchy of metrics:
+     dist n → type_dist2 n → dist_later n → type_dist2_later. *)
+  Lemma type_dist_dist2 n ty1 ty2 : dist n ty1 ty2 → type_dist2 n ty1 ty2.
+  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.
+    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.
+  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.
+  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.
+
+  Lemma ty_size_type_dist n : Proper (type_dist2 n ==> eq) ty_size.
+  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.
+  Lemma ty_shr_type_dist n :
+    Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
+  Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
+End type_dist2.
+
+(** Type-nonexpansive and Type-contractive functions. *)
+(* Note that TypeContractive is neither weaker nor stronger than Contractive, because
+   (a) it allows the dependency of own on shr to be non-expansive, and
+   (b) it forces the dependency of shr on own to be doubly-contractive.
+   It would be possible to weaken this so that no double-contractivity is required.
+   However, then it is no longer possible to write TypeContractive as just a
+   Proper, which makes it significantly more annoying to use.
+   For similar reasons, TypeNonExpansive is incomparable to NonExpansive.
+*)
+Notation TypeNonExpansive T := (∀ n, Proper (type_dist2 n ==> type_dist2 n) T).
+Notation TypeContractive T := (∀ n, Proper (type_dist2_later n ==> type_dist2 n) T).
+
+Section type_contractive.
+  Context `{typeG Σ}.
+
+  Lemma type_ne_dist_later T :
+    TypeNonExpansive T → ∀ n, Proper (type_dist2_later n ==> type_dist2_later n) T.
+  Proof. intros Hf [|n]; last exact: Hf. hnf. by intros. Qed.
+
+  (* From the above, it easily follows that TypeNonExpansive functions compose with
+     TypeNonExpansive and with TypeContractive functions. *)
+  Lemma type_ne_ne_compose T1 T2 :
+    TypeNonExpansive T1 → TypeNonExpansive T2 → TypeNonExpansive (T1 ∘ T2).
+  Proof. intros NE1 NE2 ? ???; simpl. apply: NE1. exact: NE2. Qed.
+
+  Lemma type_contractive_compose_right T1 T2 :
+    TypeContractive T1 → TypeNonExpansive T2 → TypeContractive (T1 ∘ T2).
+  Proof. intros HT1 HT2 ? ???. apply: HT1. exact: type_ne_dist_later. Qed.
+
+  Lemma type_contractive_compose_left T1 T2 :
+    TypeNonExpansive T1 → TypeContractive T2 → TypeContractive (T1 ∘ T2).
+  Proof. intros HT1 HT2 ? ???; simpl. apply: HT1. exact: HT2. Qed.
+
+  (* Show some more relationships between properties. *)
+  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.
+  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.
+  Qed.
+
+  (* Simple types *)
+  Global Instance ty_of_st_type_ne n :
+    Proper (dist_later n ==> type_dist2 n) ty_of_st.
+  Proof.
+    intros ???. constructor.
+    - done.
+    - intros. destruct n; first done; simpl. by f_equiv.
+    - intros. solve_contractive.
+  Qed.
+End type_contractive.
+
+(* Tactic automation. *)
+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)]
+          end ].
+Ltac solve_type_proper :=
+  constructor;
+  solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv).
+
+Section type.
+  Context `{typeG Σ}.
+
+  (** Copy types *)
+  Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
+    match n with
+    | 0%nat => ∅
+    | S n => ↑shrN.@l ∪ shr_locsE (shift_loc l 1%nat) n
+    end.
+
+  Lemma shr_locsE_shift l n m :
+    shr_locsE l (n + m) = shr_locsE l n ∪ shr_locsE (shift_loc l n) m.
+  Proof.
+    revert l; induction n; intros l.
+    - rewrite shift_loc_0. set_solver+.
+    - rewrite -Nat.add_1_l Nat2Z.inj_add /= IHn shift_loc_assoc.
+      set_solver+.
+  Qed.
+
+  Lemma shr_locsE_disj l n m :
+    shr_locsE l n ⊥ shr_locsE (shift_loc l n) m.
+  Proof.
+    revert l; induction n; intros l.
+    - simpl. set_solver+.
+    - rewrite -Nat.add_1_l Nat2Z.inj_add /=.
+      apply disjoint_union_l. split; last (rewrite -shift_loc_assoc; exact: IHn).
+      clear IHn. revert n; induction m; intros n; simpl; first set_solver+.
+      rewrite shift_loc_assoc. apply disjoint_union_r. split.
+      + apply ndot_ne_disjoint. destruct l. intros [=]. omega.
+      + rewrite -Z.add_assoc. move:(IHm (n + 1)%nat). rewrite Nat2Z.inj_add //.
+  Qed.
+
+  Lemma shr_locsE_shrN l n :
+    shr_locsE l n ⊆ ↑shrN.
+  Proof.
+    revert l; induction n=>l /=; first by set_solver+.
+    apply union_least; last by auto. solve_ndisj.
+  Qed.
+
+  Lemma shr_locsE_subseteq l n m :
+    (n ≤ m)%nat → shr_locsE l n ⊆ shr_locsE l m.
+  Proof.
+    induction 1; first done. etrans; first done.
+    rewrite -Nat.add_1_l [(_ + _)%nat]comm_L shr_locsE_shift. set_solver+.
+  Qed.
+
+  Lemma shr_locsE_split_tok l n m tid :
+    na_own tid (shr_locsE l (n + m)) ⊣⊢
+      na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (shift_loc l n) m).
+  Proof.
+    rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
+  Qed.
+
+  Class Copy (t : type) := {
+    copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
+    copy_shr_acc κ tid E F l q :
+      lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
+      lft_ctx -∗ t.(ty_shr) κ tid l -∗ na_own tid F -∗ q.[κ] ={E}=∗
+         ∃ q', na_own tid (F ∖ shr_locsE l t.(ty_size)) ∗
+           ▷(l ↦∗{q'}: t.(ty_own) tid) ∗
+        (na_own tid (F ∖ shr_locsE l t.(ty_size)) -∗ ▷l ↦∗{q'}: t.(ty_own) tid
+                                    ={E}=∗ na_own tid F ∗ q.[κ])
+  }.
+  Global Existing Instances copy_persistent.
+
+  Global Instance copy_equiv :
+    Proper (equiv ==> impl) Copy.
+  Proof.
+    intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1. split.
+    - intros. rewrite -EQown. apply _.
+    - intros *. rewrite -EQsz -EQshr. setoid_rewrite <-EQown.
+      apply copy_shr_acc.
+  Qed.
+
+  Class LstCopy (tys : list type) := lst_copy : Forall Copy tys.
+  Global Instance lst_copy_nil : LstCopy [] := List.Forall_nil _.
+  Global Instance lst_copy_cons ty tys :
+    Copy ty → LstCopy tys → LstCopy (ty::tys) := List.Forall_cons _ _ _.
+
+  Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
+  Next Obligation.
+    iIntros (st κ tid E ? l q ? HF) "#LFT #Hshr Htok Hlft".
+    iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
+    iDestruct "Hshr" as (vl) "[Hf Hown]".
+    iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
+    iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]".
+    iSplitL "Hmt1"; first by auto with iFrame.
+    iIntros "Htok2 Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
+    iDestruct ("Htok" with "Htok2") as "$".
+    iAssert (▷ ⌜length vl = length vl'⌝)%I as ">%".
+    { iNext. iDestruct (st_size_eq with "Hown") as %->.
+      iDestruct (st_size_eq with "Hown'") as %->. done. }
+    iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
+    iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
+  Qed.
+
+  (** Send and Sync types *)
+  Class Send (t : type) :=
+    send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
+
+  Global Instance send_equiv :
+    Proper (equiv ==> impl) Send.
+  Proof.
+    intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1.
+    rewrite /Send=>???. rewrite -!EQown. auto.
+  Qed.
+
+  Class LstSend (tys : list type) := lst_send : Forall Send tys.
+  Global Instance lst_send_nil : LstSend [] := List.Forall_nil _.
+  Global Instance lst_send_cons ty tys :
+    Send ty → LstSend tys → LstSend (ty::tys) := List.Forall_cons _ _ _.
+
+  Class Sync (t : type) :=
+    sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
+
+  Global Instance sync_equiv :
+    Proper (equiv ==> impl) Sync.
+  Proof.
+    intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1.
+    rewrite /Send=>????. rewrite -!EQshr. auto.
+  Qed.
+
+  Class LstSync (tys : list type) := lst_sync : Forall Sync tys.
+  Global Instance lst_sync_nil : LstSync [] := List.Forall_nil _.
+  Global Instance lst_sync_cons ty tys :
+    Sync ty → LstSync tys → LstSync (ty::tys) := List.Forall_cons _ _ _.
+
+  Global Instance ty_of_st_sync st :
+    Send (ty_of_st st) → Sync (ty_of_st st).
+  Proof.
+    iIntros (Hsend κ tid1 tid2 l). iDestruct 1 as (vl) "[Hm Hown]".
+    iExists vl. iFrame "Hm". iNext. by iApply Hsend.
+  Qed.
+End type.
+
 Section subtyping.
   Context `{typeG Σ}.
   Definition type_incl (ty1 ty2 : type) : iProp Σ :=
@@ -327,6 +472,12 @@ Section subtyping.
      (□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
 
+  Global Instance type_incl_ne : NonExpansive2 type_incl.
+  Proof.
+    intros n ?? [EQsz1%leibniz_equiv EQown1 EQshr1] ?? [EQsz2%leibniz_equiv EQown2 EQshr2].
+    rewrite /type_incl. repeat ((by auto) || f_equiv).
+  Qed.
+
   Global Instance type_incl_persistent ty1 ty2 : PersistentP (type_incl ty1 ty2) := _.
   (*  Typeclasses Opaque type_incl. *)
 
@@ -347,9 +498,6 @@ Section subtyping.
 
   Definition subtype (ty1 ty2 : type) : Prop :=
     elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ type_incl ty1 ty2.
-  (* TODO RJ: I'd really like to get rid of this definition. *)
-  Definition ctx_eq {A} (x1 x2 : A) : Prop :=
-    elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ ⌜x1 = x2⌝.
 
   Lemma subtype_refl ty : subtype ty ty.
   Proof. iIntros. iApply type_incl_refl. Qed.
@@ -362,6 +510,10 @@ Section subtyping.
     - iApply (H23 with "[] []"); done.
   Qed.
 
+  (* Conditional equality (intended to be used with sizes) *)
+  (* TODO RJ: I'd really like to get rid of this definition. *)
+  Definition ctx_eq {A} (x1 x2 : A) : Prop :=
+    elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ ⌜x1 = x2⌝.
   Lemma ctx_eq_refl {A} (x : A) : ctx_eq x x.
   Proof. by iIntros "_ _". Qed.
   Global Instance ctx_eq_equivalent {A} : Equivalence (@ctx_eq A).
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 53e18448400a1a18b632669e9b16b5ef76a4d8a0..9c7f4cc02ecd47c1f8215097857a1aee91d52289 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -79,14 +79,11 @@ Section uniq_bor.
     Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) uniq_bor.
   Proof. intros ??[]; split; by apply uniq_mono. Qed.
 
-  Global Instance uniq_contractive κ : Contractive (uniq_bor κ).
-  Proof.
-    intros n ?? EQ. constructor=> //=.
-    - destruct n=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
-    - intros κ' tid l. repeat (apply EQ || f_contractive || f_equiv).
-  Qed.
-  Global Instance uniq_ne κ n : Proper (dist n ==> dist n) (uniq_bor κ).
-  Proof. apply contractive_ne, _. Qed.
+  Global Instance uniq_type_contractive κ : TypeContractive (uniq_bor κ).
+  Proof. solve_type_proper. Qed.
+
+  Global Instance uniq_ne κ : NonExpansive (uniq_bor κ).
+  Proof. apply type_contractive_ne, _. Qed.
 
   Global Instance uniq_send κ ty :
     Send ty → Send (uniq_bor κ ty).
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 690f0f73c591396d00ad77f8cbfc7fef593b51ef..b273af62085a132d55e843c1b7279856c1a72422 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -21,11 +21,8 @@ Section cell.
     iIntros (ty ?? tid l) "#H⊑ H". by iApply (na_bor_shorten with "H⊑").
   Qed.
 
-  Global Instance cell_ne n : Proper (dist n ==> dist n) cell.
-  Proof.
-    intros ?? EQ. constructor; simpl; try apply EQ.
-    intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
-  Qed.
+  Global Instance cell_type_ne : TypeNonExpansive cell.
+  Proof. solve_type_proper. Qed.
 
   Global Instance cell_mono E L : Proper (eqtype E L ==> subtype E L) cell.
   Proof.
diff --git a/theories/typing/unsafe/refcell/ref.v b/theories/typing/unsafe/refcell/ref.v
index e524dd99ad9130c047604175ac4b255639cf3ff6..c9c8b761a4cb361e1f4f44258656a9f2c8461db2 100644
--- a/theories/typing/unsafe/refcell/ref.v
+++ b/theories/typing/unsafe/refcell/ref.v
@@ -68,14 +68,10 @@ Section ref.
     - by iApply na_bor_shorten.
   Qed.
 
-  Global Instance ref_contractive α : Contractive (ref α).
-  Proof.
-    intros n ?? EQ. unfold ref. constructor=>//=.
-    - intros tid vl. destruct n as [|n]=>//=. repeat (f_contractive || f_equiv). apply EQ.
-    - intros κ tid l. repeat (f_contractive || f_equiv). apply EQ.
-  Qed.
-  Global Instance ref_ne n α : Proper (dist n ==> dist n) (ref α).
-  Proof. apply contractive_ne, _. Qed.
+  Global Instance ref_type_contractive α : TypeContractive (ref α).
+  Proof. solve_type_proper. Qed.
+  Global Instance ref_ne α : NonExpansive (ref α).
+  Proof. apply type_contractive_ne, _. Qed.
 
   Global Instance ref_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) ref.
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 6ccdd17ea4f6ef58f4edde35ada9ce5d9d045f72..063fd5b13ebe1140562c922af13ce1260400689d 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -50,10 +50,9 @@ Section refcell_inv.
       end)%I.
 
   Global Instance refcell_inv_ne n tid l γ α :
-    Proper (dist n ==> dist n) (refcell_inv tid l γ α).
-  Proof.
-    intros ty1 ty2 Hty. unfold refcell_inv.
-    repeat (f_contractive || f_equiv || apply Hty || apply dist_S).
+    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).
   Qed.
 
   Lemma refcell_inv_proper E L tid l γ α ty1 ty2 :
@@ -149,12 +148,10 @@ Section refcell.
     iExists _, _. iFrame. iApply lft_incl_trans; auto.
   Qed.
 
-  Global Instance refcell_ne n : Proper (dist n ==> dist n) refcell.
+  Global Instance refcell_type_ne : TypeNonExpansive refcell.
   Proof.
-    move=>ty1 ty2 Hty. constructor; simpl.
-    - f_equiv. apply Hty.
-    - intros tid vl. destruct n as [|n]=>//=. repeat f_equiv. apply Hty.
-    - intros κ tid l. by repeat f_equiv.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
   Qed.
 
   Global Instance refcell_mono E L : Proper (eqtype E L ==> subtype E L) refcell.
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/unsafe/refcell/refmut.v
index f619bdaa1b8af8ede238a1e93452b49efccc0f72..2dbaf8465e5aa49de9018d724c02c887e487a900 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/unsafe/refcell/refmut.v
@@ -86,14 +86,10 @@ Section refmut.
       iApply ty_shr_mono; try done. iApply lft_glb_mono. iApply lft_incl_refl. done.
   Qed.
 
-  Global Instance refmut_contractive α : Contractive (refmut α).
-  Proof.
-    intros n ?? EQ. unfold refmut. constructor=>//=.
-    - intros tid vl. destruct n as [|n]=>//=. repeat (f_contractive || f_equiv). apply EQ.
-    - intros κ tid l. repeat (f_contractive || f_equiv). apply EQ.
-  Qed.
-  Global Instance refmut_ne n α : Proper (dist n ==> dist n) (refmut α).
-  Proof. apply contractive_ne, _. Qed.
+  Global Instance refmut_type_contractive α : TypeContractive (refmut α).
+  Proof. solve_type_proper. Qed.
+  Global Instance refmut_ne α : NonExpansive (refmut α).
+  Proof. apply type_contractive_ne, _. Qed.
 
   Global Instance refmut_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) refmut.
diff --git a/theories/typing/unsafe/rwlock/rwlock.v b/theories/typing/unsafe/rwlock/rwlock.v
index 3ce0d9f404a17aa341274155f722abe16e77740a..fcdfbe40e9c036ea73a001619ca10e5ec2b8edaf 100644
--- a/theories/typing/unsafe/rwlock/rwlock.v
+++ b/theories/typing/unsafe/rwlock/rwlock.v
@@ -47,10 +47,9 @@ Section rwlock_inv.
       end)%I.
 
   Global Instance rwlock_inv_ne n tid l γ α :
-    Proper (dist n ==> dist n) (rwlock_inv tid l γ α).
-  Proof.
-    intros ty1 ty2 Hty. unfold rwlock_inv.
-    repeat (f_contractive || f_equiv || apply Hty || apply dist_S).
+    Proper (type_dist2 n ==> dist n) (rwlock_inv tid l γ α).
+  Proof. 
+    solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
   Qed.
 
   Lemma rwlock_inv_proper E L tid l γ α ty1 ty2 :
@@ -143,12 +142,10 @@ Section rwlock.
     iExists _, _. iFrame. iApply lft_incl_trans; auto.
   Qed.
 
-  Global Instance rwlock_ne n : Proper (dist n ==> dist n) rwlock.
+  Global Instance rwlock_type_ne : TypeNonExpansive rwlock.
   Proof.
-    move=>ty1 ty2 Hty. constructor; simpl.
-    - f_equiv. apply Hty.
-    - intros tid vl. destruct n as [|n]=>//=. repeat f_equiv. apply Hty.
-    - intros κ tid l. by repeat f_equiv.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
   Qed.
 
   Global Instance rwlock_mono E L : Proper (eqtype E L ==> subtype E L) rwlock.
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard.v b/theories/typing/unsafe/rwlock/rwlockreadguard.v
index 21f9a717a50fb95fe7453e95e307197626071f03..9b773a27c7e291d6ecf140f28c3af552b7c4e426 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard.v
+++ b/theories/typing/unsafe/rwlock/rwlockreadguard.v
@@ -61,14 +61,14 @@ Section rwlockreadguard.
     iApply lft_incl_refl.
   Qed.
 
-  Global Instance rwlockreadguard_contractive α : Contractive (rwlockreadguard α).
+  Global Instance rwlockreadguard_type_contractive α : TypeContractive (rwlockreadguard α).
   Proof.
-    intros n ?? EQ. unfold rwlockreadguard. constructor=>//=.
-    - intros tid vl. destruct n as [|n]=>//=. by repeat f_equiv.
-    - intros κ tid l. repeat (f_contractive || f_equiv). apply EQ.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_ne; try reflexivity) ||
+                                              f_type_equiv || f_contractive || f_equiv).
   Qed.
-  Global Instance rwlockreadguard_ne n α : Proper (dist n ==> dist n) (rwlockreadguard α).
-  Proof. apply contractive_ne, _. Qed.
+  Global Instance rwlockreadguard_ne α : NonExpansive (rwlockreadguard α).
+  Proof. apply type_contractive_ne, _. Qed.
 
   (* The rust type is not covariant, although it probably could (cf. refcell).
      This would require changing the definition of the type, though. *)
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard.v b/theories/typing/unsafe/rwlock/rwlockwriteguard.v
index 15ad051c8daa29e8ed4d376f31fa3bc20a0550e1..9386c022a103ce67ecb6188e71ac7969ca715793 100644
--- a/theories/typing/unsafe/rwlock/rwlockwriteguard.v
+++ b/theories/typing/unsafe/rwlock/rwlockwriteguard.v
@@ -73,15 +73,14 @@ Section rwlockwriteguard.
       iApply ty_shr_mono; try done. iApply lft_glb_mono. iApply lft_incl_refl. done.
   Qed.
 
-  Global Instance rwlockwriteguard_contractive α : Contractive (rwlockwriteguard α).
+  Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
   Proof.
-    intros n ?? EQ. unfold rwlockwriteguard. constructor=>//=.
-    - intros tid vl. destruct n as [|n]=>//=.
-      do 9 f_equiv. solve_contractive. by repeat f_equiv.
-    - intros κ tid l. repeat (f_contractive || f_equiv). apply EQ.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_ne; try reflexivity) ||
+                                              f_type_equiv || f_contractive || f_equiv).
   Qed.
   Global Instance rwlockwriteguard_ne α : NonExpansive (rwlockwriteguard α).
-  Proof. apply contractive_ne, _. Qed.
+  Proof. apply type_contractive_ne, _. Qed.
 
   Global Instance rwlockwriteguard_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) rwlockwriteguard.