diff --git a/iris_core.v b/iris_core.v
index 748de892f8095762440300938722e29faf311b88..11ecbd696135a157eaf22bb1bb5d93b0af140dbc 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -18,8 +18,8 @@ Module Type IRIS_RES (RL : RA_T) (C : CORE_LANG) <: RA_T.
   Instance res_valid: RA_valid res := _.
   Instance res_ra   : RA res := _.
 
-  (* Make this explicit. It would otherwise infer the order on pairs. *)
-  Instance res_pord: preoType res := pord_ra (T := res).
+  (* Make this explicit. It may otherwise use the order on pairs. *)
+  Instance res_pord: preoType res := pord_ra.
 End IRIS_RES.
 Module IrisRes (RL : RA_T) (C : CORE_LANG) <: IRIS_RES RL C.
   Include IRIS_RES RL C. (* I cannot believe Coq lets me do this... *)
diff --git a/lib/ModuRes/BI.v b/lib/ModuRes/BI.v
index 497e463ddebc4a308fd260127938ca4f77a71501..08d855834f450497613611f8c75192b1d9d1809f 100644
--- a/lib/ModuRes/BI.v
+++ b/lib/ModuRes/BI.v
@@ -741,20 +741,7 @@ Section MComplMM.
 
   Section Def.
     Context U `{pcmU : pcmType U} {eU : extensible U}.
-
-    Program Instance extensible_prod : extensible (U * V) :=
-      mkExtend (fun uv1 uv2 => (extend (fst uv1) (fst uv2), extend (snd uv1) (snd uv2))).
-    Next Obligation.
-      destruct vd as [ud vd]; destruct ve as [ue ve].
-      destruct HD as [HDu HDv]; destruct HS as [HSu HSv].
-      split; eapply extend_dist; eassumption.
-    Qed.
-    Next Obligation.
-      destruct vd as [ud vd]; destruct ve as [ue ve].
-      destruct HD as [HDu HDv]; destruct HS as [HSu HSv].
-      split; eapply extend_sub; eassumption.
-    Qed.
-
+    
     Program Definition mclose_mm : (U -n> V -m> B) -n> U -m> V -m> B :=
       n[(fun f => mcurry (mclose n[(fun uv => f (fst uv) (snd uv))]))].
     Next Obligation.
diff --git a/lib/ModuRes/CBUltInst.v b/lib/ModuRes/CBUltInst.v
index e25fed0996197b5abcb06f243615fa0fad92c409..1225ffc3b74df696a35898d667d824ceec02a50b 100644
--- a/lib/ModuRes/CBUltInst.v
+++ b/lib/ModuRes/CBUltInst.v
@@ -2,7 +2,7 @@
     bisected, ultrametric spaces, forms an M-category. *)
 
 Require Import CSetoid.
-Require Import MetricCore MetricRec.
+Require Import MetricCore CatBasics MetricRec.
 
 Module CBUlt <: MCat.
   Local Open Scope cat_scope.
diff --git a/lib/ModuRes/MetricCore.v b/lib/ModuRes/MetricCore.v
index 9b463e89b837948c883c21fed724a5cca11bdb72..3404e940b36bfa06837c22ba18dd6f53ea2e0bbd 100644
--- a/lib/ModuRes/MetricCore.v
+++ b/lib/ModuRes/MetricCore.v
@@ -252,15 +252,15 @@ Section MMInst.
 
 (*
   (** Note the set of morphisms, not the set of non-expansive maps. The distance is the supremum of pointwise distances. *)
-  Global Program Instance fundistS : Dist (M -s> N) :=
+  Global Program Instance fundistS : Dist (M -s> N) | 5 :=
     fun n f g => forall x, f x = n = g x.
 
   (** Note the set of non-expansive maps with the point-wise distance. *)
-  Global Program Instance fundist : Dist (M -n> N) :=
+  Global Program Instance fundist : Dist (M -n> N) | 5:=
     fun n f g => met_morph f = n = met_morph g.
 
   (** The hom-set (i.e. the set of non-expansive maps) is again a bisected ultrametic spaces. *)
-  Global Instance MMmetric : metric (M -n> N) (D := fundist).
+  Global Instance MMmetric : metric (M -n> N) (D := fundist) | 5.
   Proof.
     split.
     + split; [intros HEq t | intros HEq n].
@@ -554,7 +554,7 @@ Section MetricProducts.
     fst p1 = n = fst p2 /\ snd p1 = n = snd p2.
   Global Arguments prod_dist n p1 p2 /.
 
-  Global Program Instance prod_metric : metric (U * V) := mkMetr prod_dist.
+  Global Program Instance prod_metric : metric (U * V) | 5 := mkMetr prod_dist.
   Next Obligation.
     intros [a1 b1] [a2 b2] [Ha Hb] [a3 b3] [a4 b4] [Ha' Hb']; simpl in *.
     rewrite Ha, Hb, Ha', Hb'; reflexivity.
@@ -610,7 +610,7 @@ Section MetricProducts.
     (compl (liftc Mfst σ), compl (liftc Msnd σ)).
   Arguments prod_compl σ σc /.
 
-  Global Program Instance prod_cmetric : cmetric (U * V) :=
+  Global Program Instance prod_cmetric : cmetric (U * V) | 5 :=
     mkCMetr prod_compl.
   Next Obligation.
     intros n; destruct (conv_cauchy (liftc Mfst σ) n) as [mfst Hfst].
@@ -662,7 +662,7 @@ Section OptM.
                end
       end.
 
-  Global Program Instance option_metric : metric (option T) :=
+  Global Program Instance option_metric : metric (option T) | 5 :=
     mkMetr option_dist.
   Next Obligation.
     destruct n as [| n]; intros [x |] [y |] EQxy [u |] [v |] EQuv; simpl in *; try (contradiction || reflexivity); [].
@@ -700,7 +700,7 @@ Section Submetric.
   Definition subset_Dist n (x y : {e : T | P e}) := proj1_sig x = n = proj1_sig y.
   Global Arguments subset_Dist n x y /.
 
-  Global Program Instance sub_metric : metric {e : T | P e} :=
+  Global Program Instance sub_metric : metric {e : T | P e} | 5 :=
     mkMetr subset_Dist.
   Next Obligation.
     intros [x Hx] [y Hy] EQxy [u Hu] [v Hv] EQuv; unfold equiv in EQxy, EQuv; simpl in *.
@@ -743,7 +743,7 @@ Section SubCMetric.
 
   Definition sub_compl (σ : chain {x : T | P x}) {σc : cchain σ} :=
     exist P (compl (liftc inclM σ)) (subchainlubP σ).
-  Global Program Instance sub_cmetric : cmetric {x : T | P x} :=
+  Global Program Instance sub_cmetric : cmetric {x : T | P x} | 5 :=
     mkCMetr sub_compl.
   Next Obligation.
     intros n; simpl; destruct (conv_cauchy (liftc inclM σ) n) as [m Hm].
@@ -810,7 +810,7 @@ Section DiscreteMetric.
     end.
   Global Arguments discreteDist n x y / .
   
-  Program Instance discreteMetric : metric T := mkMetr discreteDist.
+  Program Instance discreteMetric : metric T | 10 := mkMetr discreteDist.
   Next Obligation.
     intros x y Heq x' y' Heq'. split; (destruct n as [|n]; [reflexivity|simpl]).
     - intros Heqx. rewrite <-Heq, <-Heq'. assumption.
@@ -833,7 +833,7 @@ Section DiscreteMetric.
 
   Definition discreteCompl (σ : chain T) {σc : cchain σ} := σ 1.
 
-  Program Instance discreteCMetric : cmetric T := mkCMetr discreteCompl.
+  Program Instance discreteCMetric : cmetric T | 10 := mkCMetr discreteCompl.
   Next Obligation.
     intros n; exists 1; simpl; intros [| i] HLe; [inversion HLe |].
     destruct n as [| n]; [exact I |].
@@ -877,7 +877,7 @@ Section Option.
       | Some v => Some (compl (unSome σ _))
     end.
 
-  Global Program Instance option_cmt : cmetric (option T) := mkCMetr option_compl.
+  Global Program Instance option_cmt : cmetric (option T) | 5 := mkCMetr option_compl.
   Next Obligation.
     intros [| n]; [exists 0; intros; apply dist_bound | unfold option_compl].
     generalize (@eq_refl _ (σ 1)) as EQ1; pattern (σ 1) at 1 3; destruct (σ 1) as [v |]; intros.
diff --git a/lib/ModuRes/PCBUltInst.v b/lib/ModuRes/PCBUltInst.v
index 372d19e6bde51d56df3747cd3ecbbd9b6833741a..a40762cb959e471d930a695178a9fd1e2884557e 100644
--- a/lib/ModuRes/PCBUltInst.v
+++ b/lib/ModuRes/PCBUltInst.v
@@ -3,7 +3,7 @@
     M-category. *)
 
 Require Import PreoMet.
-Require Import MetricRec.
+Require Import CatBasics MetricRec.
 
 Module PCBUlt <: MCat.
   Local Obligation Tactic := intros; resp_set || mono_resp || eauto with typeclass_instances.
diff --git a/lib/ModuRes/Predom.v b/lib/ModuRes/Predom.v
index 5ca114b5aa043af436d46c03329c25b139cd2d40..1ce91b37a21120ab914f6377761e567f879d4a69 100644
--- a/lib/ModuRes/Predom.v
+++ b/lib/ModuRes/Predom.v
@@ -53,9 +53,9 @@ Section MMorphProps1.
     - move=> f1 f2 EQf t. by symmetry.
     - move=> f1 f2 f3 EQ12 EQ23 t. by transitivity (f2 t).
   Qed.
-  Global Instance mon_morph_type : Setoid (T -m> U) := mkType mon_morph_eq.
+  Global Instance mon_morph_type : Setoid (T -m> U) | 5 := mkType mon_morph_eq.
 
-  Global Program Instance mon_morph_preoT : preoType (T -m> U) :=
+  Global Program Instance mon_morph_preoT : preoType (T -m> U) | 5 :=
     mkPOType (fun f g => forall x, f x ⊑ g x) _.
   Next Obligation.
     split.
@@ -115,7 +115,7 @@ Section MonotoneProducts.
 
   Definition prod_ord (p1 p2 : U * V) := (fst p1 ⊑ fst p2) /\ (snd p1 ⊑ snd p2).
 
-  Global Program Instance preoType_prod : preoType (U * V) := mkPOType prod_ord _.
+  Global Program Instance preoType_prod : preoType (U * V) | 5 := mkPOType prod_ord _.
   Next Obligation.
     split.
     - intros [a b]; split; simpl; reflexivity.
@@ -292,7 +292,7 @@ Section SubPredom.
 
   Definition subset_ord (x y : {t : T | P t}) := proj1_sig x ⊑ proj1_sig y.
   Arguments subset_ord _ _ /.
-  Global Program Instance subset_preo : preoType {a : T | P a} := mkPOType subset_ord _.
+  Global Program Instance subset_preo : preoType {a : T | P a} | 5 := mkPOType subset_ord _.
   Next Obligation.
     split.
     - intros [x Hx]; red; simpl; reflexivity.
@@ -327,6 +327,70 @@ End SubPredom.
 
 Global Arguments subset_ord {_ _ _ _} _ _ /.
 
+(** Preorders on option types.
+
+    Caution: this is *one* of the ways to define the order, and not necessarily the only useful.
+    Thus, the instances are local, and should be declared w/ Existing Instance where needed. *)
+Section Option.
+  Context `{pcV : preoType V}.
+
+  (* The preorder on options where None is the bottom element. *)
+  Section Bot.
+
+    Definition option_pord_bot (o1 o2 : option V) :=
+      match o1 with
+        | None => True
+        | Some v1 => match o2 with
+                       | None => False
+                       | Some v2 => pord v1 v2
+                     end
+      end.
+    Program Instance option_preo_bot : preoType (option V) | 5 := mkPOType option_pord_bot _.
+    Next Obligation.
+      split.
+      - intros [v |]; simpl; [reflexivity | exact I].
+      - intros [v1 |] [v2 |] [v3 |] Sub12 Sub23; simpl in *; try exact I || contradiction; [].
+        etransitivity; eassumption.
+    Qed.
+    Next Obligation.
+      move=> x1 x2 Rx y1 y2 Ry; move: Rx Ry.
+      case: x1=>[x1|]; case: x2=>[x2|] //= Rx.
+      case: y1=>[y1|]; case: y2=>[y2|] //= Ry; last done.
+      by rewrite Rx Ry; reflexivity.
+    Qed.
+
+  End Bot.
+
+  (* And the preorder, where None is a top element *)
+  Section Top.
+
+    Definition option_pord_top (o1 o2 : option V) :=
+      match o2 with
+        | None => True
+        | Some v2 => match o1 with
+                       | None => False
+                       | Some v1 => pord v1 v2
+                     end
+      end.
+    Program Instance option_preo_top : preoType (option V) | 5 := mkPOType option_pord_top _.
+    Next Obligation.
+      split.
+      - intros [v |]; simpl; [reflexivity | exact I].
+      - intros [v1 |] [v2 |] [v3 |] Sub12 Sub23; simpl in *; try exact I || contradiction; [].
+        etransitivity; eassumption.
+    Qed.
+    Next Obligation.
+      move=> x1 x2 Rx y1 y2 Ry; move: Rx Ry.
+      case: x1=>[x1|]; case: x2=>[x2|] //= Rx;
+      case: y1=>[y1|]; case: y2=>[y2|] //= Ry; last done.
+      rewrite Rx Ry; by reflexivity.
+    Qed.
+      
+  End Top.
+
+End Option.
+
+
 Section ViewLemmas.
   Context {T} `{oT : preoType T}.
   Implicit Types (t : T).
diff --git a/lib/ModuRes/PreoMet.v b/lib/ModuRes/PreoMet.v
index 09683ec5ef57f9ae95c37ac4472f93481fdf7b6b..e082eac758f4a89a3ba461ff6aa11823a6f0ba24 100644
--- a/lib/ModuRes/PreoMet.v
+++ b/lib/ModuRes/PreoMet.v
@@ -297,7 +297,7 @@ Section MonotoneProducts.
   Context `{pcT : pcmType T} `{pcU : pcmType U} `{pcV : pcmType V}.
   Local Obligation Tactic := intros; apply _ || mono_resp || program_simpl.
 
-  Global Instance pcmType_prod : pcmType (U * V).
+  Global Instance pcmType_prod : pcmType (U * V) | 5.
   Proof.
     split.
     - intros [a1 b1] [a2 b2] [Ha12 Hb12] [a3 b3] [a4 b4] [Ha34 Hb34].
@@ -431,7 +431,7 @@ Section SubPCM.
   Program Definition p1sNE :=
     n[(fun x : {a : T | P a} => proj1_sig x)].
 
-  Global Instance pcmType_sub : pcmType {a : T | P a}.
+  Global Instance pcmType_sub : pcmType {a : T | P a} | 5.
   Proof.
     split.
     - intros [x HPx] [y HPy] EQxy [u HPu] [v HPv] EQuv; simpl in *.
@@ -471,29 +471,9 @@ Section Option.
   (* The preorder on options where None is the bottom element. *)
   Section Bot.
 
-    Definition option_pord_bot (o1 o2 : option V) :=
-      match o1 with
-        | None => True
-        | Some v1 => match o2 with
-                       | None => False
-                       | Some v2 => v1 ⊑ v2
-                     end
-      end.
-    Program Instance option_preo_bot : preoType (option V) := mkPOType option_pord_bot _.
-    Next Obligation.
-      split.
-      - intros [v |]; simpl; [reflexivity | exact I].
-      - intros [v1 |] [v2 |] [v3 |] Sub12 Sub23; simpl in *; try exact I || contradiction; [].
-        etransitivity; eassumption.
-    Qed.
-    Next Obligation.
-      move=> x1 x2 Rx y1 y2 Ry; move: Rx Ry.
-      case: x1=>[x1|]; case: x2=>[x2|] //= Rx.
-      case: y1=>[y1|]; case: y2=>[y2|] //= Ry; last done.
-      by rewrite Rx Ry; reflexivity.
-    Qed.
+    Existing Instance option_preo_bot.
 
-    Instance option_pcm_bot : pcmType (option V).
+    Instance option_pcm_bot : pcmType (option V) | 5.
     Proof.
       split.
       - intros o1 o2 EQ12 o3 o4 EQ34; split; intros HS.
@@ -529,29 +509,9 @@ Section Option.
   (* And the preorder, where None is a top element *)
   Section Top.
 
-    Definition option_pord_top (o1 o2 : option V) :=
-      match o2 with
-        | None => True
-        | Some v2 => match o1 with
-                       | None => False
-                       | Some v1 => v1 ⊑ v2
-                     end
-      end.
-    Program Instance option_preo_top : preoType (option V) := mkPOType option_pord_top _.
-    Next Obligation.
-      split.
-      - intros [v |]; simpl; [reflexivity | exact I].
-      - intros [v1 |] [v2 |] [v3 |] Sub12 Sub23; simpl in *; try exact I || contradiction; [].
-        etransitivity; eassumption.
-    Qed.
-    Next Obligation.
-      move=> x1 x2 Rx y1 y2 Ry; move: Rx Ry.
-      case: x1=>[x1|]; case: x2=>[x2|] //= Rx;
-      case: y1=>[y1|]; case: y2=>[y2|] //= Ry; last done.
-      rewrite Rx Ry; by reflexivity.
-    Qed.
-      
-    Instance option_pcm_top : pcmType (option V).
+    Existing Instance option_preo_top.
+
+    Instance option_pcm_top : pcmType (option V) | 5.
     Proof.
       split.
       - intros o1 o2 EQ12 o3 o4 EQ34; split; intros HS.
@@ -629,7 +589,6 @@ Section ExtOrdDiscrete.
 End ExtOrdDiscrete.
 
 Section ExtProd.
-  (* FIXME This is a duplicate of stuf in BI.v: There's also an "extensible_prod" there. *)
   Context T U `{ET : extensible T} `{EU : extensible U}. 
 
   Global Instance prod_extensible : extensible (T * U) := mkExtend (fun s s' => pair (extend (fst s) (fst s')) (extend (snd s) (snd s'))).
diff --git a/world_prop.v b/world_prop.v
index cce80cff1078f13ec0805ccc8584123895dc6418..1d52b3971d2404869578c7c0461133f00ee969fc 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -1,7 +1,7 @@
 (** In this file, we we define what it means to be a solution of the recursive
     domain equations to build a higher-order separation logic *)
-Require Import ModuRes.PreoMet.
-Require Import ModuRes.Finmap ModuRes.Constr.
+Require Import ModuRes.PreoMet ModuRes.Finmap.
+Require Import ModuRes.CatBasics. (* Get the "halve" functor. This brings in bundled types... *)
 Require Import ModuRes.RA ModuRes.UPred.
 
 (* This interface keeps some of the details of the solution opaque *)
diff --git a/world_prop_recdom.v b/world_prop_recdom.v
index 5d67bb3d55e55adde8b4560184b5037fd5dbe5e2..36764a1df0148bf48a8f22d3e65dc26495c4d945 100644
--- a/world_prop_recdom.v
+++ b/world_prop_recdom.v
@@ -1,8 +1,7 @@
 (** In this file, we show how we can obtain a solution of the recursive
     domain equations to build a higher-order separation logic *)
-Require Import ModuRes.PreoMet ModuRes.MetricRec ModuRes.CBUltInst.
-Require Import ModuRes.Finmap ModuRes.Constr.
-Require Import ModuRes.RA ModuRes.UPred.
+Require Import ModuRes.PreoMet ModuRes.Finmap ModuRes.RA ModuRes.UPred.
+Require Import ModuRes.CatBasics ModuRes.MetricRec ModuRes.CBUltInst.
 Require Import world_prop.
 
 (* Now we come to the actual implementation *)