diff --git a/opam.pins b/opam.pins
index 5957dcd0f0dfa15f933e9513f50fdae25362df04..202664902296013ad5d1896abfca2d49917d8de5 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 5180d1cd4548b2ae5193fe9e76b97cbf6ffbc345
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1e241cca15302ae89d41f14251c2dafbd7efebb6
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 308fb5177e25fbfa86861804870e345fe6e86262..e2f2e057f5ca001d66fd4eb7611149d33660a804 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -8,7 +8,7 @@ Section fixpoint_def.
   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.
@@ -19,7 +19,7 @@ Section fixpoint_def.
 End fixpoint_def.
 
 Lemma type_fixpoint_ne `{typeG Σ} (T1 T2 : type → type)
-  `{!TypeContractive T1, !TypeContractive T2} n :
+    `{!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.
 
@@ -36,15 +36,14 @@ Section fixpoint.
     - exists bool. apply _.
     - done.
     - (* 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.
+         use limit_preserving_and directly. However, on the Coq side, it is
+         more convenient as a record -- so this is where we pay. *)
+      eapply (limit_preserving_ext (λ _, _ ∧ _)).
+      { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
+      apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
+      { apply uPred.limit_preserving_PersistentP; solve_proper. }
+      apply limit_preserving_impl, uPred.limit_preserving_entails;
+        solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
 
   Global Instance fixpoint_send :
@@ -55,7 +54,8 @@ Section fixpoint.
     - apply send_equiv.
     - exists bool. apply _.
     - done.
-    - intros c Hc ???. entails_lim c; [solve_proper..|]. intros n. apply Hc.
+    - repeat (apply limit_preserving_forall=> ?).
+      apply uPred.limit_preserving_entails; solve_proper.
   Qed.
 
   Global Instance fixpoint_sync :
@@ -66,7 +66,8 @@ Section fixpoint.
     - apply sync_equiv.
     - exists bool. apply _.
     - done.
-    - intros c Hc ????. entails_lim c; [solve_proper..|]. intros n. apply Hc.
+    - repeat (apply limit_preserving_forall=> ?).
+      apply uPred.limit_preserving_entails; solve_proper.
   Qed.
 
   Lemma fixpoint_unfold_eqtype E L : eqtype E L (type_fixpoint T) (T (type_fixpoint T)).
@@ -90,8 +91,8 @@ Section subtyping.
     - intros ?? EQ ?. etrans; last done. by apply equiv_subtype.
     - by eexists _.
     - intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12.
-    - intros c Hc. rewrite /subtype. entails_lim c; [solve_proper..|].
-      intros n. apply Hc.
+    - repeat (apply limit_preserving_forall=> ?).
+      apply uPred.limit_preserving_entails; solve_proper.
   Qed.
 
   Lemma fixpoint_proper T1 `{TypeContractive T1} T2 `{TypeContractive T2} :
@@ -103,11 +104,10 @@ Section subtyping.
     - intros ?? EQ ?. etrans; last done. by apply equiv_eqtype.
     - by eexists _.
     - 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.
+    - apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?);
+        apply uPred.limit_preserving_entails; solve_proper.
   Qed.
 
-  (* 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.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index d46e6ddf712943a2822b3fde81ad6dd3c4fc6e5e..c2405089595102274cfbb3fb8ea75bf811775977 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -90,7 +90,7 @@ Section rc.
         iExists _, _, _. iFrame. done. }
       iDestruct "HX" as (γ ν q') "(#Hinv & Hrc & Htok & #Hshr)".
       iMod ("Hclose2" with "[] [Hrc Htok]") as "[HX Htok]".
-      { iNext. iIntros "HX". iModIntro. (* FIXME: iNext here doesn't strip of the next from in front of the evar. *)
+      { iNext. iIntros "HX". iModIntro. iNext.
         iRight. iExists γ, ν, q'. iExact "HX". }
       { iNext. by iFrame "#∗". }
       iAssert (|={F ∖ ↑shrN}=> C)%I with "[HX]" as ">#HC".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 9f53f4c187e1318dfa3385a90ff4cfeeb4aae12b..5ef44d371e164eb3ffe28dcb59eda9b05c5408ca 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -7,8 +7,6 @@ Set Default Proof Using "Type".
 Section sum.
   Context `{typeG Σ}.
 
-  Local Obligation Tactic := idtac.
-
   Program Definition emp : type :=
     {| ty_size := 1%nat;
        ty_own tid vl := False%I;
@@ -207,11 +205,10 @@ Section sum.
       { rewrite <-HF. simpl. rewrite <-union_subseteq_r.
         apply shr_locsE_subseteq. omega. }
       iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
-      { (* Really, we don't even have a lemma for anti-monotonicity of difference...? *)
-        cut (shr_locsE (shift_loc l 1) (ty_size (nth i tyl ∅)) ⊆
-                  shr_locsE (shift_loc l 1) (list_max (map ty_size tyl))).
-        - simpl. set_solver+.
-        - apply shr_locsE_subseteq. omega. }
+      { apply difference_mono_l.
+        trans (shr_locsE (shift_loc l 1) (list_max (map ty_size tyl))).
+        - apply shr_locsE_subseteq. omega.
+        - set_solver+. }
       destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
       rewrite -(heap_mapsto_pred_op _ q' q'02); last (by intros; apply ty_size_eq).
       rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index e083ca78c3704aa0513b55acb4f72637427fba05..6c34dabf165607c2aa39adfa6d96b137d8b9d276 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -152,23 +152,16 @@ Section ofe.
 
   Global Instance type_cofe : Cofe typeC.
   Proof.
-    apply: (iso_cofe_subtype P type_pack type_unpack).
+    apply (iso_cofe_subtype' P type_pack type_unpack).
+    - by intros [].
     - 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.
-        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.
-        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.
-        apply equiv_dist, uPred.entails_equiv_and, ty_shr_mono.
+    - (* TODO: automate this *)
+      repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?).
+      + apply uPred.limit_preserving_PersistentP=> n ty1 ty2 Hty; apply Hty.
+      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty.
+      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
+      + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
   Qed.
 
   Inductive st_equiv' (ty1 ty2 : simple_type) : Prop :=
@@ -333,16 +326,56 @@ Ltac solve_type_proper :=
   constructor;
   solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv).
 
+
+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.
+
+Class Copy `{typeG Σ} (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.[κ])
+}.
+Existing Instances copy_persistent.
+Instance: Params (@Copy) 2.
+
+Class LstCopy `{typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
+Instance: Params (@LstCopy) 2.
+Global Instance lst_copy_nil `{typeG Σ} : LstCopy [] := List.Forall_nil _.
+Global Instance lst_copy_cons `{typeG Σ} ty tys :
+  Copy ty → LstCopy tys → LstCopy (ty :: tys) := List.Forall_cons _ _ _.
+
+Class Send `{typeG Σ} (t : type) :=
+  send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
+Instance: Params (@Send) 2.
+
+Class LstSend `{typeG Σ} (tys : list type) := lst_send : Forall Send tys.
+Instance: Params (@LstSend) 2.
+Global Instance lst_send_nil `{typeG Σ} : LstSend [] := List.Forall_nil _.
+Global Instance lst_send_cons `{typeG Σ} ty tys :
+  Send ty → LstSend tys → LstSend (ty :: tys) := List.Forall_cons _ _ _.
+
+Class Sync `{typeG Σ} (t : type) :=
+  sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
+Instance: Params (@Sync) 2.
+
+Class LstSync `{typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
+Instance: Params (@LstSync) 2.
+Global Instance lst_sync_nil `{typeG Σ} : LstSync [] := List.Forall_nil _.
+Global Instance lst_sync_cons `{typeG Σ} ty tys :
+  Sync ty → LstSync tys → LstSync (ty :: tys) := List.Forall_cons _ _ _.
+
 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.
@@ -386,20 +419,7 @@ Section type.
     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.
+  Global Instance copy_equiv : Proper (equiv ==> impl) Copy.
   Proof.
     intros ty1 ty2 [EQsz%leibniz_equiv EQown EQshr] Hty1. split.
     - intros. rewrite -EQown. apply _.
@@ -407,11 +427,6 @@ Section type.
       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".
@@ -430,50 +445,43 @@ Section type.
   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.
+  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.
+  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).
+  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 Σ :=
+Definition type_incl `{typeG Σ} (ty1 ty2 : type) : iProp Σ :=
     (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
      (□ ∀ 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.
+Instance: Params (@type_incl) 2.
+(* Typeclasses Opaque type_incl. *)
+
+Definition subtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+  elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ type_incl ty1 ty2.
+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.
+Instance: Params (@eqtype) 4.
+
+Section subtyping.
+  Context `{typeG Σ}.
 
   Global Instance type_incl_ne : NonExpansive2 type_incl.
   Proof.
@@ -482,7 +490,6 @@ Section subtyping.
   Qed.
 
   Global Instance type_incl_persistent ty1 ty2 : PersistentP (type_incl ty1 ty2) := _.
-  (*  Typeclasses Opaque type_incl. *)
 
   Lemma type_incl_refl ty : type_incl ty ty.
   Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
@@ -497,31 +504,20 @@ Section subtyping.
     - iApply "Hs23". iApply "Hs12". done.
   Qed.
 
-  Context (E : elctx) (L : llctx).
-
-  Definition subtype (ty1 ty2 : type) : Prop :=
-    elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ type_incl ty1 ty2.
-
-  Lemma subtype_refl ty : subtype ty ty.
+  Lemma subtype_refl E L ty : subtype E L ty ty.
   Proof. iIntros. iApply type_incl_refl. Qed.
-  Global Instance subtype_preorder : PreOrder subtype.
+  Global Instance subtype_preorder E L : PreOrder (subtype E L).
   Proof.
     split; first by intros ?; apply subtype_refl.
     intros ty1 ty2 ty3 H12 H23. iIntros.
-    iApply (type_incl_trans with "[] []").
-    - iApply (H12 with "[] []"); done.
-    - iApply (H23 with "[] []"); done.
+    iApply type_incl_trans. by iApply H12. by iApply H23.
   Qed.
 
-  Lemma equiv_subtype ty1 ty2 : ty1 ≡ ty2 → subtype ty1 ty2.
+  Lemma equiv_subtype E L ty1 ty2 : ty1 ≡ ty2 → subtype E L ty1 ty2.
   Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.
 
-  (* TODO: The prelude should have a symmetric closure. *)
-  Definition eqtype (ty1 ty2 : type) : Prop :=
-    subtype ty1 ty2 ∧ subtype ty2 ty1.
-
-  Lemma eqtype_unfold ty1 ty2 :
-    eqtype ty1 ty2 ↔
+  Lemma eqtype_unfold E L ty1 ty2 :
+    eqtype E L ty1 ty2 ↔
     (elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
       (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
       (□ ∀ tid vl, ty1.(ty_own) tid vl ↔ ty2.(ty_own) tid vl) ∗
@@ -545,17 +541,17 @@ Section subtyping.
       + iIntros "!#* H". by iApply "Hshr".
   Qed.
 
-  Lemma eqtype_refl ty : eqtype ty ty.
+  Lemma eqtype_refl E L ty : eqtype E L ty ty.
   Proof. by split. Qed.
 
-  Lemma equiv_eqtype ty1 ty2 : ty1 ≡ ty2 → eqtype ty1 ty2.
+  Lemma equiv_eqtype E L ty1 ty2 : ty1 ≡ ty2 → eqtype E L ty1 ty2.
   Proof. by split; apply equiv_subtype. Qed.
 
-  Global Instance subtype_proper :
-    Proper (eqtype ==> eqtype ==> iff) subtype.
+  Global Instance subtype_proper E L :
+    Proper (eqtype E L ==> eqtype E L ==> iff) (subtype E L).
   Proof. intros ??[] ??[]. split; intros; by etrans; [|etrans]. Qed.
 
-  Global Instance eqtype_equivalence : Equivalence eqtype.
+  Global Instance eqtype_equivalence E L : Equivalence (eqtype E L).
   Proof.
     split.
     - by split.
@@ -563,21 +559,16 @@ Section subtyping.
     - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
   Qed.
 
-  Lemma subtype_simple_type (st1 st2 : simple_type) :
+  Lemma subtype_simple_type E L (st1 st2 : simple_type) :
     (∀ tid vl, elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
                  st1.(st_own) tid vl -∗ st2.(st_own) tid vl) →
-    subtype st1 st2.
+    subtype E L st1 st2.
   Proof.
     intros Hst. iIntros. iSplit; first done. iSplit; iAlways.
     - iIntros. iApply Hst; done.
-    - iIntros (???) "H".
-      iDestruct "H" as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
+    - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
       by iApply Hst.
   Qed.
-End subtyping.
-
-Section weakening.
-  Context `{typeG Σ}.
 
   Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :
     E1 ⊆+ E2 → L1 ⊆+ L2 →
@@ -589,7 +580,7 @@ Section weakening.
     - iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
       eauto using elem_of_submseteq.
   Qed.
-End weakening.
+End subtyping.
 
 Hint Resolve subtype_refl eqtype_refl : lrust_typing.
 Hint Opaque subtype eqtype : lrust_typing.