diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index b2f7533aa597463bb2590e53215ea3f846d45af8..33089d3beba49b86df5037b5956196f88b9432a0 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -300,7 +300,8 @@ Section code.
         * iExists _. iFrame "Hl2". destruct weak.
           -- iLeft. iSplit; first done. rewrite Hincls. iFrame "Hl†".
              iMod (own_update_2 with "Hst Htok") as "Hst".
-             { apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
+             { apply auth_update_dealloc.
+               rewrite -{1}(right_id ((None, 0%nat) : prodUR _ _) _ (_, _)).
                apply cancel_local_update_unit, _. }
              rewrite -[in (1).[ν]%I]Hqq' -[(|={lft_userE,⊤}=>_)%I]fupd_trans.
              iApply step_fupd_mask_mono;
@@ -362,7 +363,8 @@ Section code.
           -- iLeft. iFrame. iSplitR; first done.
              iApply ("Hclose" with "[>- $Hna]"). iExists (None, 0%nat).
              iMod (own_update_2 with "Hst Htok") as "$"; last done.
-             apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
+             apply auth_update_dealloc.
+             rewrite -{1}(right_id ((None, 0%nat) : prodUR _ _) _ (_, _)).
              apply cancel_local_update_unit, _.
           -- iRight. iSplitR; first by auto with lia. iIntros "!> Hl† Hl2 Hvl".
              iApply ("Hclose" with "[>- $Hna]"). iExists (None, S weak).
@@ -381,7 +383,7 @@ Section code.
           iFrame. iExists _. iFrame. auto with iFrame.
         * iMod (own_update_2 with "Hst Htok") as "Hst".
           { apply auth_update_dealloc.
-            rewrite pair_op Cinl_op Some_op -{1}(left_id 0%nat _ weak) pair_op.
+            rewrite pair_op Cinl_op Some_op -{1}(left_id (0%nat : natUR) _ weak) pair_op.
             apply (cancel_local_update_unit _ (_, _)). }
           iApply "Hclose". iFrame "Hna Hst". iExists (q+q'')%Qp. iFrame.
           iSplitL; first last.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1245b1d6596fff91999003112fb4c5ea9bf0c2d5..ef7aca70ba0bb97ae5a67a0665b0ca818edde179 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -301,8 +301,8 @@ 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. eapply dist_later_fin_iff. destruct n; first done.
-    split; intros; try apply EQ; try si_solver.
+    intros EQ. dist_later_fin_intro.
+    split; intros; try apply EQ; eauto using SIdx.lt_succ_diag_r.
     apply dist_S, EQ.
   Qed.
   Lemma type_later_dist2_later n ty1 ty2 : dist_later n ty1 ty2 → type_dist2_later n ty1 ty2.
@@ -316,7 +316,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. si_solver. Qed.
+  Proof. intros ?? EQ ??-> ??->. apply EQ, SIdx.lt_succ_diag_r. Qed.
   Lemma ty_shr_type_dist n :
     Proper (type_dist2 n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
   Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
@@ -382,9 +382,7 @@ 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 =>
-                            eapply dist_later_fin_iff; destruct n as [|n]; [exact I|change (@dist A _ n x y)]
-          end ].
+          dist_later_fin_intro ].
 Ltac solve_type_proper :=
   constructor;
   solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive_fin || f_equiv).
@@ -484,7 +482,7 @@ Section type.
 
   Global Instance copy_equiv : Proper (equiv ==> impl) Copy.
   Proof.
-    intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1. split.
+    intros ty1 ty2 [EQsz EQown EQshr] Hty1. split.
     - intros. rewrite -EQown. apply _.
     - intros *. rewrite -EQsz -EQshr. setoid_rewrite <-EQown.
       apply copy_shr_acc.
@@ -510,13 +508,13 @@ Section type.
   (** Send and Sync types *)
   Global Instance send_equiv : Proper (equiv ==> impl) Send.
   Proof.
-    intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1.
+    intros ty1 ty2 [EQsz EQown EQshr] Hty1.
     rewrite /Send=>???. rewrite -!EQown. auto.
   Qed.
 
   Global Instance sync_equiv : Proper (equiv ==> impl) Sync.
   Proof.
-    intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1.
+    intros ty1 ty2 [EQsz EQown EQshr] Hty1.
     rewrite /Send=>????. rewrite -!EQshr. auto.
   Qed.
 
@@ -552,26 +550,18 @@ Definition type_equal `{!typeG Σ} (ty1 ty2 : type) : vProp Σ :=
      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l ∗-∗ ty2.(ty_shr) κ tid l))%I.
 Global Instance: Params (@type_equal) 2 := {}.
 
-Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
-  ∀ qmax qL, llctx_interp_noend qmax L qL ⊢ □ (elctx_interp E -∗ type_incl ty1 ty2).
-Global Instance: Params (@subtype) 4 := {}.
-
-(* TODO: The prelude should have a symmetric closure. *)
-Definition eqtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
-  subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
-Global Instance: Params (@eqtype) 4 := {}.
-
-Section subtyping.
+Section iprop_subtyping.
   Context `{!typeG Σ}.
 
   Global Instance type_incl_ne : NonExpansive2 type_incl.
   Proof.
-    intros n ?? [EQsz1%leibniz_equiv EQown1 EQshr1] ?? [EQsz2%leibniz_equiv EQown2 EQshr2].
+    intros n ?? [EQsz1 EQown1 EQshr1] ?? [EQsz2 EQown2 EQshr2].
     rewrite /type_incl. repeat ((by auto) || f_equiv).
   Qed.
 
   Global Instance type_incl_persistent ty1 ty2 : Persistent (type_incl ty1 ty2) := _.
 
+  
   Lemma type_incl_refl ty : ⊢ type_incl ty ty.
   Proof. iSplit; first done. iSplit; iModIntro; iIntros; done. Qed.
 
@@ -585,6 +575,92 @@ Section subtyping.
     - iApply "Hs23". iApply "Hs12". done.
   Qed.
 
+  Global Instance type_equal_ne : NonExpansive2 type_equal.
+  Proof.
+    intros n ?? [EQsz1 EQown1 EQshr1] ?? [EQsz2 EQown2 EQshr2].
+    rewrite /type_equal. repeat ((by auto) || f_equiv).
+  Qed.
+  Global Instance type_equal_proper :
+    Proper ((≡) ==> (≡) ==> (⊣⊢)) type_equal.
+  Proof. apply ne_proper_2, _. Qed.
+
+  Global Instance type_equal_persistent ty1 ty2 : Persistent (type_equal ty1 ty2) := _.
+
+  Lemma type_equal_incl ty1 ty2 :
+    type_equal ty1 ty2 ⊣⊢ type_incl ty1 ty2 ∗ type_incl ty2 ty1.
+  Proof.
+    iSplit.
+    - iIntros "#(% & Ho & Hs)".
+      iSplit; (iSplit; first done; iSplit; iModIntro).
+      + iIntros (??) "?". by iApply "Ho".
+      + iIntros (???) "?". by iApply "Hs".
+      + iIntros (??) "?". by iApply "Ho".
+      + iIntros (???) "?". by iApply "Hs".
+    - iIntros "#[(% & Ho1 & Hs1) (% & Ho2 & Hs2)]".
+      iSplit; first done. iSplit; iModIntro.
+      + iIntros (??). iSplit; [iApply "Ho1"|iApply "Ho2"].
+      + iIntros (???). iSplit; [iApply "Hs1"|iApply "Hs2"].
+  Qed.
+
+  Lemma type_equal_refl ty :
+    ⊢ type_equal ty ty.
+  Proof.
+    iApply type_equal_incl. iSplit; iApply type_incl_refl.
+  Qed.
+  Lemma type_equal_trans ty1 ty2 ty3 :
+    type_equal ty1 ty2 -∗ type_equal ty2 ty3 -∗ type_equal ty1 ty3.
+  Proof.
+    rewrite !type_equal_incl. iIntros "#[??] #[??]". iSplit.
+    - iApply (type_incl_trans _ ty2); done.
+    - iApply (type_incl_trans _ ty2); done.
+  Qed.
+
+  Lemma type_incl_simple_type (st1 st2 : simple_type) :
+    □ (∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl) -∗
+    type_incl st1 st2.
+  Proof.
+    iIntros "#Hst". iSplit; first done. iSplit; iModIntro.
+    - iIntros. iApply "Hst"; done.
+    - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
+      by iApply "Hst".
+  Qed.
+
+  Lemma type_equal_equiv ty1 ty2 :
+    (⊢ type_equal ty1 ty2) ↔ ty1 ≡ ty2.
+  Proof.
+    split.
+    - intros Heq. split.
+      + eapply uPred.pure_soundness, embed_emp_valid_inj.
+        iDestruct Heq as "[%Hsz _]". done.
+      + iDestruct Heq as "[_ [Hown _]]". done.
+      + iDestruct Heq as "[_ [_ Hshr]]". done.
+    - intros ->. apply type_equal_refl.
+  Qed.
+
+End iprop_subtyping.
+
+
+(** Prop-level conditional type inclusion/equality
+    (may depend on assumptions in [E, L].) *)
+Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+  ∀ qmax qL, llctx_interp_noend qmax L qL ⊢ □ (elctx_interp E -∗ type_incl ty1 ty2).
+Global Instance: Params (@subtype) 4 := {}.
+
+(* TODO: The prelude should have a symmetric closure. *)
+Definition eqtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+  subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
+Global Instance: Params (@eqtype) 4 := {}.
+
+Section subtyping.
+  Context `{!typeG Σ}.
+
+  Lemma type_incl_subtype ty1 ty2 E L :
+    (⊢ type_incl ty1 ty2) → subtype E L ty1 ty2.
+  Proof.
+    intros Heq. rewrite /subtype.
+    iIntros (??) "_ !> _". done.
+  Qed.
+
   Lemma subtype_refl E L ty : subtype E L ty ty.
   Proof. iIntros (??) "_ !> _". iApply type_incl_refl. Qed.
   Global Instance subtype_preorder E L : PreOrder (subtype E L).
@@ -635,35 +711,6 @@ Section subtyping.
     iApply type_incl_refl.
   Qed.
 
-  Lemma type_equal_incl ty1 ty2 :
-    type_equal ty1 ty2 ⊣⊢ type_incl ty1 ty2 ∗ type_incl ty2 ty1.
-  Proof.
-    iSplit.
-    - iIntros "#(% & Ho & Hs)".
-      iSplit; (iSplit; first done; iSplit; iModIntro).
-      + iIntros (??) "?". by iApply "Ho".
-      + iIntros (???) "?". by iApply "Hs".
-      + iIntros (??) "?". by iApply "Ho".
-      + iIntros (???) "?". by iApply "Hs".
-    - iIntros "#[(% & Ho1 & Hs1) (% & Ho2 & Hs2)]".
-      iSplit; first done. iSplit; iModIntro.
-      + iIntros (??). iSplit; [iApply "Ho1"|iApply "Ho2"].
-      + iIntros (???). iSplit; [iApply "Hs1"|iApply "Hs2"].
-  Qed.
-
-  Lemma type_equal_refl ty :
-    ⊢ type_equal ty ty.
-  Proof.
-    iApply type_equal_incl. iSplit; iApply type_incl_refl.
-  Qed.
-  Lemma type_equal_trans ty1 ty2 ty3 :
-    type_equal ty1 ty2 -∗ type_equal ty2 ty3 -∗ type_equal ty1 ty3.
-  Proof.
-    rewrite !type_equal_incl. iIntros "#[??] #[??]". iSplit.
-    - iApply (type_incl_trans _ ty2); done.
-    - iApply (type_incl_trans _ ty2); done.
-  Qed.
-
   Lemma lft_invariant_eqtype E L T :
     Proper (lctx_lft_eq E L ==> eqtype E L) T.
   Proof. split; by apply lft_invariant_subtype. Qed.
@@ -717,16 +764,6 @@ Section subtyping.
     - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
   Qed.
 
-  Lemma type_incl_simple_type (st1 st2 : simple_type) :
-    □ (∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl) -∗
-    type_incl st1 st2.
-  Proof.
-    iIntros "#Hst". iSplit; first done. iSplit; iModIntro.
-    - iIntros. iApply "Hst"; done.
-    - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
-      by iApply "Hst".
-  Qed.
-
   Lemma subtype_simple_type E L (st1 st2 : simple_type) :
     (∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗
        ∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl)) →