diff --git a/theories/typing/function.v b/theories/typing/function.v
index 55183c084441e6af707216957917af0489a3b39e..4071d4c64c60de00115d8df6a5e7010570fd25f1 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -76,7 +76,8 @@ Section fn.
     intros tid vl. unfold typed_body.
     do 12 f_equiv. f_contractive. do 16 ((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 /=. repeat (apply Hfp || f_equiv).
+      rewrite !tctx_interp_singleton /tctx_elt_interp /=.
+      do 5 f_equiv. apply type_dist2_dist. apply Hfp.
     - rewrite /tctx_interp !big_sepL_zip_with /=. do 4 f_equiv.
       cut (∀ n tid p i, Proper (dist n ==> dist n)
         (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 7e63812f56227aa0bfa85448d08519518ee5fdd7..86f711a810a82c17c139e55bdd832f061d988113 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -590,8 +590,8 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (rc ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hx". iFrame "Hr†". iExists [_].
-      rewrite heap_mapsto_vec_singleton /=. eauto 10 with iFrame. }
+      unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
+      rewrite heap_mapsto_vec_singleton /=. simpl. eauto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 90b45aec53bb2b13d94d5efe1a0ef33a5f06ed56..456d4a80cafc08efd632f5527d20fcdcfdb0e114 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -279,7 +279,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hx". iFrame "Hr†". iExists [_].
+      unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
       rewrite heap_mapsto_vec_singleton /=. eauto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -352,7 +352,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton /=.
+      unlock. iFrame. iExists [# #l']. rewrite heap_mapsto_vec_singleton /=.
       auto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index a7b8630ed089d617243c536d50ade4d91555d8b4..7267fbf52e63801c2a7c32238c1faf87c8973b70 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -137,7 +137,7 @@ Section rwlockreadguard_functions.
       iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lx' ◁ rwlockreadguard α ty]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
-                tctx_hasty_val' //=. auto 10 with iFrame. }
+                tctx_hasty_val' //=; simpl. auto 10 with iFrame. }
       iApply type_jump; solve_typing.
   Qed.
 End rwlockreadguard_functions.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 9b2a19aebea0f470b0b56b88a8acd1f59d60f6e2..aa4fc4149d7af8e3fd8c586eb6721f54ce66d689 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -51,7 +51,7 @@ Instance: Params (@ty_size) 2.
 Instance: Params (@ty_own) 2.
 Instance: Params (@ty_shr) 2.
 
-Arguments ty_own {_ _} _ _ !_ /.
+Arguments ty_own {_ _} _ _ !_ / : simpl nomatch.
 
 Class TyWf `{typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
 Arguments ty_lfts {_ _} _ {_}.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 33dbb662b9cca63f308f2d9172fe8178464be112..dfa4a4385c64a0525797b506339fa9f0ec443cc1 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -31,15 +31,15 @@ Section case.
     edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
     wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
     destruct Hety as [Hety|Hety]; iApply (Hety with "LFT HE Hna HL HC");
-      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
-    - iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //=; iFrame "HT".
+    - rewrite /own_ptr /=. iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
       iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
       + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_mapsto_vec_singleton.
         iFrame. iExists [_], []. auto.
-      + iFrame. iExists _. iFrame.
+      + eauto with iFrame.
       + rewrite -EQlen app_length minus_plus -(shift_loc_assoc_nat _ 1).
         iFrame. iExists _. iFrame. rewrite uninit_own. auto.
-    - rewrite -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
+    - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
       iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
       iFrame. iExists i, vl', vl''. rewrite /= -EQlen app_length nth_lookup EQty /=. auto.
   Qed.