diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index bfe1304145495e02fec2d60814e00c865db71049..308fb5177e25fbfa86861804870e345fe6e86262 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -18,6 +18,11 @@ Section fixpoint_def.
   Definition type_fixpoint : type := fixpointK 2 T.
 End fixpoint_def.
 
+Lemma type_fixpoint_ne `{typeG Σ} (T1 T2 : type → type)
+  `{!TypeContractive T1, !TypeContractive T2} n :
+  (∀ t, T1 t ≡{n}≡ T2 t) → type_fixpoint T1 ≡{n}≡ type_fixpoint T2.
+Proof. eapply fixpointK_ne; apply type_contractive_ne, _. Qed.
+
 Section fixpoint.
   Context `{typeG Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 86916b7e57b38da8ccfd11d31fa594d7fa750d56..5a27d299b491583561519c03a94f85a89aa73daa 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -71,6 +71,13 @@ Section product.
     Proper (type_dist2 n ==> type_dist2 n ==> type_dist2 n) product2.
   Proof. solve_type_proper. Qed.
 
+  Global Instance product2_ne :
+    NonExpansive2 product2.
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
   Global Instance product2_mono E L:
     Proper (subtype E L ==> subtype E L ==> subtype E L) product2.
   Proof.
@@ -141,6 +148,8 @@ Section 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_ne : NonExpansive product.
+  Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
   Global Instance product_mono E L:
     Proper (Forall2 (subtype E L) ==> subtype E L) product.
   Proof. intros ??. induction 1=>//=. by f_equiv. Qed.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 0d598a27de6b3e71e486658100814f5408c3f534..ef3d107d990804de3ce656c77875793c2f48a6aa 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -95,7 +95,7 @@ Section sum.
     - iApply ((nth i tyl ∅).(ty_shr_mono) with "Hord"); done.
   Qed.
 
-  Global Instance sum_type_ne n: Proper (Forall2 (type_dist2 n) ==> type_dist2 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)).
@@ -113,6 +113,24 @@ Section sum.
       solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
   Qed.
 
+  Global Instance sum_ne : NonExpansive sum.
+  Proof.
+    intros n 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. }
+    (* 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_dist n (nth i x ∅) (nth i y ∅)).
+    { clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
+    constructor; simpl.
+    - by rewrite EQmax.
+    - intros tid vl. rewrite EQmax.
+      solve_proper_core ltac:(fun _ => exact:EQnth || f_equiv).
+    - intros κ tid l. unfold is_pad. rewrite EQmax.
+      solve_proper_core ltac:(fun _ => exact:EQnth || (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
   Global Instance sum_mono E L :
     Proper (Forall2 (subtype E L) ==> subtype E L) sum.
   Proof.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index b273af62085a132d55e843c1b7279856c1a72422..76dcf3236685287540b40a30f06eb06432d4dbe8 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -24,6 +24,11 @@ Section cell.
   Global Instance cell_type_ne : TypeNonExpansive cell.
   Proof. solve_type_proper. Qed.
 
+  Global Instance cell_ne : NonExpansive cell.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
+  Qed.
+
   Global Instance cell_mono E L : Proper (eqtype E L ==> subtype E L) cell.
   Proof.
     iIntros (?? EQ%eqtype_unfold) "#HE #HL".
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/unsafe/refcell/refcell.v
index 063fd5b13ebe1140562c922af13ce1260400689d..aa8ee23e2da8bb2a90f5ad154dc0c26fd27287e2 100644
--- a/theories/typing/unsafe/refcell/refcell.v
+++ b/theories/typing/unsafe/refcell/refcell.v
@@ -49,12 +49,18 @@ Section refcell_inv.
              end
       end)%I.
 
-  Global Instance refcell_inv_ne n tid l γ α :
+  Global Instance refcell_inv_type_ne n tid l γ α :
     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.
 
+  Global Instance refcell_inv_ne tid l γ α : NonExpansive (refcell_inv tid l γ α).
+  Proof.
+    intros n ???. (* TODO: f_equiv takes forever here, what is going on? *)
+    eapply refcell_inv_type_ne, type_dist_dist2. done.
+  Qed.
+
   Lemma refcell_inv_proper E L tid l γ α ty1 ty2 :
     eqtype E L ty1 ty2 →
     elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
@@ -151,7 +157,13 @@ Section refcell.
   Global Instance refcell_type_ne : TypeNonExpansive refcell.
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply refcell_inv_type_ne; try reflexivity) ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance refcell_ne : NonExpansive refcell.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || f_equiv).
   Qed.
 
   Global Instance refcell_mono E L : Proper (eqtype E L ==> subtype E L) refcell.
diff --git a/theories/typing/unsafe/rwlock/rwlock.v b/theories/typing/unsafe/rwlock/rwlock.v
index fcdfbe40e9c036ea73a001619ca10e5ec2b8edaf..177721457d5fa4072b03d5c776d9aa0f60913e32 100644
--- a/theories/typing/unsafe/rwlock/rwlock.v
+++ b/theories/typing/unsafe/rwlock/rwlock.v
@@ -46,12 +46,17 @@ Section rwlock_inv.
       | _ => (* Locked for write. *) True
       end)%I.
 
-  Global Instance rwlock_inv_ne n tid l γ α :
+  Global Instance rwlock_inv_type_ne n tid l γ α :
     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.
 
+  Global Instance rwlock_inv_ne tid l γ α : NonExpansive (rwlock_inv tid l γ α).
+  Proof.
+    intros n ???. eapply rwlock_inv_type_ne, type_dist_dist2. done.
+  Qed.
+
   Lemma rwlock_inv_proper E L tid l γ α ty1 ty2 :
     eqtype E L ty1 ty2 →
     elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
@@ -145,7 +150,13 @@ Section rwlock.
   Global Instance rwlock_type_ne : TypeNonExpansive rwlock.
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_type_ne; try reflexivity) ||
+                                              f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance rwlock_ne : NonExpansive rwlock.
+  Proof.
+    constructor; solve_proper_core ltac:(fun _ => (eapply ty_size_ne; try reflexivity) || 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 9b773a27c7e291d6ecf140f28c3af552b7c4e426..01076b7a99cfa049151112c86ae3443dc2475167 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard.v
+++ b/theories/typing/unsafe/rwlock/rwlockreadguard.v
@@ -64,7 +64,7 @@ Section rwlockreadguard.
   Global Instance rwlockreadguard_type_contractive α : TypeContractive (rwlockreadguard α).
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_ne; try reflexivity) ||
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_type_ne; try reflexivity) ||
                                               f_type_equiv || f_contractive || f_equiv).
   Qed.
   Global Instance rwlockreadguard_ne α : NonExpansive (rwlockreadguard α).
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard.v b/theories/typing/unsafe/rwlock/rwlockwriteguard.v
index 9386c022a103ce67ecb6188e71ac7969ca715793..660d3fd955aafd81d2154b4f665773d0f9fc97ec 100644
--- a/theories/typing/unsafe/rwlock/rwlockwriteguard.v
+++ b/theories/typing/unsafe/rwlock/rwlockwriteguard.v
@@ -76,7 +76,7 @@ Section rwlockwriteguard.
   Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
   Proof.
     constructor;
-      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_ne; try reflexivity) ||
+      solve_proper_core ltac:(fun _ => exact: type_dist2_S || (eapply rwlock_inv_type_ne; try reflexivity) ||
                                               f_type_equiv || f_contractive || f_equiv).
   Qed.
   Global Instance rwlockwriteguard_ne α : NonExpansive (rwlockwriteguard α).