diff --git a/iris_plog.v b/iris_plog.v
index 92957efa229bbd11502dc4b5fe53d720a3eb8574..66727a9d5bc154aa332cff2b0fe3d7bf07f8abfb 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -23,7 +23,7 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
     (** Invariants **)
     Definition invP i P w : UPred res :=
-      intEq (w i) (Some (ı' P)) w.
+      intEq (w i) (Some (ı' (halved P))) w.
     Program Definition inv i : Props -n> Props :=
       n[(fun P => m[(invP i P)])].
     Next Obligation.
@@ -41,7 +41,7 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
     Qed.
     Next Obligation.
       intros p1 p2 EQp w; unfold invP.
-      cut ((w i === Some (ı' p1)) = n = (w i === Some (ı' p2))).
+      cut ((w i === Some (ı' (halved p1))) = n = (w i === Some (ı' (halved p2)))).
       { intros Heq. now eapply Heq. }
       eapply met_morph_nonexp.
       now eapply dist_mono, (met_morph_nonexp ı').
@@ -120,7 +120,7 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
                       /\ forall i (Hm : m i),
                            (i ∈ dom rs <-> i ∈ dom w) /\
                            forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
-                             ı π w n ri) _).
+                             (unhalved (ı π)) w n ri) _).
     Next Obligation.
       intros n1 n2 _ _ HLe _ [rs [HLS HRS] ]. exists rs; split; [assumption|].
       setoid_rewrite HLe; eassumption.
@@ -146,15 +146,16 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
         intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
         assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
         destruct (w1 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
-        apply ı in EQπ; apply EQπ; [now auto with arith |].
-        apply (met_morph_nonexp (ı π')) in EQw; apply EQw; [omega |].
+        apply ı in EQπ. apply halve_eq in EQπ.
+        apply EQÏ€; [now auto with arith |].
+        apply (met_morph_nonexp (unhalved (ı π'))) in EQw; apply EQw; [omega |].
         apply HR; [reflexivity | assumption].
       - split; [assumption | split; [rewrite (domeq EQw); apply HM, Hm |] ].
         intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
         assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
-        destruct (w2 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
-        apply ı in EQπ; apply EQπ; [now auto with arith |].
-        apply (met_morph_nonexp (ı π')) in EQw; apply EQw; [omega |].
+        destruct (w2 i) as [Ï€' |]; [| contradiction]. do 3 red in EQÏ€.
+        apply ı in EQπ. apply halve_eq in EQπ. apply EQπ; [now auto with arith |].
+        apply (met_morph_nonexp (unhalved (ı π'))) in EQw; apply EQw; [omega |].
         apply HR; [reflexivity | assumption].
     Qed.
 
diff --git a/iris_vs_rules.v b/iris_vs_rules.v
index b12434f14aef08e4e5843dbebee05825d6b8a8ef..2d4b90f2e479889f3e2c124e3822d98b859f55c2 100644
--- a/iris_vs_rules.v
+++ b/iris_vs_rules.v
@@ -29,11 +29,9 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       (inv i P) ⊑ pvs (mask_sing i) mask_emp (▹P).
     Proof.
       intros w n r HInv w'; intros.
-      change (match w i with Some x => x = S n = ı' P | None => False end) in HInv.
+      change (match w i with Some x => x = S n = ı' (halved P) | None => False end) in HInv.
       destruct (w i) as [μ |] eqn: HLu; [| contradiction].
-      apply ı in HInv; rewrite ->(isoR P) in HInv.
-      (* get rid of the invisible 1/2 *)
-      do 8 red in HInv.
+      apply ı in HInv; rewrite ->(isoR (halved P)) in HInv.
       destruct HE as [rs [HE HM] ].
       destruct (rs i) as [ri |] eqn: HLr.
       - rewrite ->comp_map_remove with (i := i) (r := ri) in HE by now eapply equivR.
@@ -41,7 +39,7 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         exists w' (r · ri).
         split; [reflexivity |].
         split.
-        + simpl; eapply HInv; [now auto with arith |].
+        + simpl. apply halve_eq in HInv. eapply HInv; [now auto with arith |].
           eapply uni_pred, HM with i;
             [| exists r | | | rewrite HLr]; try reflexivity.
           * left; unfold mask_sing, mask_set.
@@ -64,11 +62,10 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       (inv i P ∧ ▹P) ⊑ pvs mask_emp (mask_sing i) ⊤.
     Proof.
       intros w n r [HInv HP] w'; intros.
-      change (match w i with Some x => x = S n = ı' P | None => False end) in HInv.
+      change (match w i with Some x => x = S n = ı' (halved P) | None => False end) in HInv.
       destruct (w i) as [μ |] eqn: HLu; [| contradiction].
-      apply ı in HInv; rewrite ->(isoR P) in HInv.
-      (* get rid of the invisible 1/2 *)
-      do 8 red in HInv.
+      apply ı in HInv; rewrite ->(isoR (halved P)) in HInv.
+      apply halve_eq in HInv.
       destruct HE as [rs [HE HM] ].
       exists w' 1; split; [reflexivity | split; [exact I |] ].
       rewrite ->(comm r), <-assoc in HE.
@@ -226,13 +223,13 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       destruct n as [| n]; [now inversion HLe | simpl in HP].
       rewrite ->HSub in HP; clear w HSub; rename w' into w.
       destruct (fresh_region w m HInf) as [i [Hm HLi] ].
-      assert (HSub : w ⊑ fdUpdate i (ı' P) w).
+      assert (HSub : w ⊑ fdUpdate i (ı' (halved P)) w).
       { intros j; destruct (Peano_dec.eq_nat_dec i j); [subst j; rewrite HLi; exact I|].
         now rewrite ->fdUpdate_neq by assumption.
       }
-      exists (fdUpdate i (ı' P) w) 1; split; [assumption | split].
+      exists (fdUpdate i (ı' (halved P)) w) 1; split; [assumption | split].
       - exists (exist _ i Hm).
-        change (((fdUpdate i (ı' P) w) i) = S (S k) = (Some (ı' P))).
+        change (((fdUpdate i (ı' (halved P)) w) i) = S (S k) = (Some (ı' (halved P)))).
         rewrite fdUpdate_eq; reflexivity.
       - erewrite ra_op_unit by apply _.
         destruct HE as [rs [HE HM] ].
diff --git a/lib/ModuRes/CBUltInst.v b/lib/ModuRes/CBUltInst.v
index 1225ffc3b74df696a35898d667d824ceec02a50b..c452cd82b918d63d8a3303bd49a40f6984b3792b 100644
--- a/lib/ModuRes/CBUltInst.v
+++ b/lib/ModuRes/CBUltInst.v
@@ -64,34 +64,44 @@ Section Halving_Fun.
   Context F {FA : BiFMap F} {FFun : BiFunctor F}.
   Local Obligation Tactic := intros; resp_set || eauto.
 
-  Program Instance halveFMap : BiFMap (fun T1 T2 => halve (F T1 T2)) :=
-    fun m1 m2 m3 m4 => lift2m (lift2s (fun ars ob => fmorph (F := F) ars ob) _ _) _ _.
+  Definition HF := fun T1 T2 => halveCM (F T1 T2).
+
+  Program Instance halveFMap : BiFMap HF :=
+    fun m1 m2 m3 m4 => lift2m (lift2s (fun (ars: (m2 -t> m1) * (m3 -t> m4)) (ob: halveCM (F m1 m3)) => halvedT (fmorph (F := F) ars (unhalvedT ob))) _ _) _ _.
+  Next Obligation.
+    repeat intro. unfold halvedT, unhalvedT, HF in *. simpl.
+    unhalveT. simpl. rewrite H. reflexivity.
+  Qed.
   Next Obligation.
     intros p1 p2 EQp x; simpl; rewrite EQp; reflexivity.
   Qed.
   Next Obligation.
-    intros e1 e2 EQ; simpl. unhalve.
-    rewrite EQ; reflexivity.
+    intros e1 e2 EQ; simpl. unfold halvedT, unhalvedT, HF in *. unhalveT.
+    destruct n as [|n]; first by exact I.
+    simpl in *. rewrite EQ; reflexivity.
   Qed.
   Next Obligation.
-    intros p1 p2 EQ e; simpl; unhalve.
-    apply dist_mono in EQ.
-    rewrite EQ; reflexivity.
+    intros p1 p2 EQ e; simpl. unfold halvedT, unhalvedT, HF in *. unhalveT.
+    destruct n as [|n]; first by exact I. simpl.
+    apply dist_mono. rewrite EQ. reflexivity.
   Qed.
 
-  Instance halveF : BiFunctor (fun T1 T2 => halve (F T1 T2)).
+  Instance halveF : BiFunctor HF.
   Proof.
     split; intros.
     + intros T; simpl.
+      unfold unhalvedT, HF in *. unhalveT. simpl.
       apply (fmorph_comp _ _ _ _ _ _ _ _ _ _ T).
     + intros T; simpl.
+      unfold unhalvedT, HF in *. unhalveT. simpl.
       apply (fmorph_id _ _ T).
   Qed.
 
   Instance halve_contractive {m0 m1 m2 m3} :
-    contractive (@fmorph _ _ (fun T1 T2 => halve (F T1 T2)) _ m0 m1 m2 m3).
+    contractive (@fmorph _ _ HF _ m0 m1 m2 m3).
   Proof.
     intros n p1 p2 EQ f; simpl.
+    unfold unhalvedT, HF in *. unhalveT. simpl.
     change ((fmorph (F := F) p1) f = n = (fmorph p2) f).
     rewrite EQ; reflexivity.
   Qed.
@@ -109,18 +119,18 @@ Module Type SimplInput(Cat : MCat).
 End SimplInput.
 
 Module InputHalve (S : SimplInput (CBUlt)) : InputType(CBUlt)
-    with Definition F := fun T1 T2 => halve (S.F T1 T2).
+    with Definition F := fun T1 T2 => halveCM (S.F T1 T2).
   Import CBUlt.
   Local Existing Instance S.FArr.
   Local Existing Instance S.FFun.
   Local Open Scope cat_scope.
 
-  Definition F T1 T2 := halve (S.F T1 T2).
+  Definition F T1 T2 := halveCM (S.F T1 T2).
   Definition FArr := halveFMap S.F.
   Definition FFun := halveF S.F.
 
   Definition tmorph_ne : 1 -t> F 1 1 :=
-    umconst (S.F_ne tt : F 1 1).
+    umconst (halvedT (S.F_ne tt)).
 
   Definition F_contractive := @halve_contractive S.F _.
 End InputHalve.
diff --git a/lib/ModuRes/CatBasics.v b/lib/ModuRes/CatBasics.v
index f8d8f176e9a2e206121b7e0875107b5c48518efe..02126ad50f0defeb2b8ff67d250aefda57845724 100644
--- a/lib/ModuRes/CatBasics.v
+++ b/lib/ModuRes/CatBasics.v
@@ -251,63 +251,18 @@ Section IndexedProductsPCM.
 End IndexedProductsPCM.
 
 
-
 Section Halving.
-  Context (T : cmtyp).
-
-  Definition dist_halve n :=
-    match n with
-      | O  => fun (_ _ : T) => True
-      | S n => dist n
-    end.
-
-  Program Definition halve_metr : metric T := mkMetr dist_halve.
-  Next Obligation.
-    destruct n; [resp_set | simpl; apply _].
-  Qed.
-  Next Obligation.
-    split; intros HEq.
-    - apply dist_refl; intros n; apply (HEq (S n)).
-    - intros [| n]; [exact I |]; revert n; apply dist_refl, HEq.
-  Qed.
-  Next Obligation.
-    intros t1 t2 HEq; destruct n; [exact I |]; symmetry; apply HEq.
-  Qed.
-  Next Obligation.
-    intros t1 t2 t3 HEq12 HEq23; destruct n; [exact I |]; etransitivity; [apply HEq12 | apply HEq23].
-  Qed.
-  Next Obligation.
-    destruct n; [exact I | apply dist_mono, H].
-  Qed.
-
-  Definition halveM : Mtyp := Build_Mtyp T halve_metr.
-
-  Instance halve_chain (σ : chain halveM) {σc : cchain σ} : cchain (fun n => σ (S n) : T).
-  Proof.
-    unfold cchain; intros.
-    apply (chain_cauchy σ σc (S n)); auto with arith.
-  Qed.
-
-  Definition compl_halve (σ : chain halveM) (σc : cchain σ) :=
-    compl (fun n => σ (S n)) (σc := halve_chain σ).
-
-  Program Definition halve_cm : cmetric halveM := mkCMetr compl_halve.
-  Next Obligation.
-    intros [| n]; [exists 0; intros; exact I |].
-    destruct (conv_cauchy _ (σc := halve_chain σ) n) as [m HCon].
-    exists (S m); intros [| i] HLe; [inversion HLe |].
-    apply HCon; auto with arith.
-  Qed.
-
-  Definition halve : cmtyp := Build_cmtyp halveM halve_cm.
+  Definition halveT (T: eqType): eqType := fromType (halve T).
+  Definition halvedT {T}: eqtyp T -> eqtyp (halveT T) := fun h => halved h.
+  Definition unhalvedT {T}: eqtyp (halveT T) -> eqtyp T := fun h => unhalved h.
 
+  Definition halveM (T: Mtyp) : Mtyp := Build_Mtyp (halveT T) halve_metr.
+  Definition halveCM (T: cmtyp): cmtyp := Build_cmtyp (halveM T) halve_cm.
 End Halving.
+Ltac unhalveT := repeat (unhalve || match goal with
+                       | x: eqtyp (mtyp (cmm (halveCM _))) |- _ => destruct x as [x]
+                       end).
 
-Ltac unhalve :=
-  match goal with
-    | |- dist_halve _ ?n ?f ?g => destruct n as [| n]; [exact I | change (f = n = g) ]
-    | |- ?f = ?n = ?g => destruct n as [| n]; [exact I | change (f = n = g) ]
-  end.
 
 (** Trivial extension of a nonexpansive morphism to monotone one on a
     metric space equipped with a trivial preorder. *)
diff --git a/lib/ModuRes/MetricCore.v b/lib/ModuRes/MetricCore.v
index 59d3c94b3b96746e669b6b51dfef17d74880b89e..0b8b1d2ec8ea98afcb301e055f783d4b15b887c9 100644
--- a/lib/ModuRes/MetricCore.v
+++ b/lib/ModuRes/MetricCore.v
@@ -379,6 +379,97 @@ End MCompP.
 
 Arguments umid T {eqT mT}.
 
+Section Halving.
+  Context {T: Type} `{cmT : cmetric T}.
+
+  CoInductive halve := halved: T -> halve.
+  Definition unhalved (h: halve) := match h with halved t => t end.
+
+  Definition dist_halve n :=
+    match n with
+      | O  => fun _ _ => True
+      | S n => fun h1 h2 => match h1, h2 with halved t1, halved t2 => dist n t1 t2 end
+    end.
+
+  Global Program Instance halve_ty : Setoid halve :=
+    mkType (fun h1 h2 =>  match h1, h2 with halved t1, halved t2 => t1 == t2 end).
+  Next Obligation.
+    split; repeat intro;
+      repeat (match goal with [ x : halve |- _ ] => destruct x end).
+    - reflexivity.
+    - symmetry; assumption.
+    - etransitivity; eassumption.
+  Qed.
+
+  Global Instance unhalve_proper : Proper (equiv ==> equiv) unhalved.
+  Proof.
+    repeat intro. repeat (match goal with [ x : halve |- _ ] => destruct x end).
+    simpl in *. assumption.
+  Qed.
+
+  Global Program Instance halve_metr : metric halve := mkMetr dist_halve.
+  Next Obligation.
+    destruct n; [now resp_set | repeat intro ];
+      repeat (match goal with [ x : halve |- _ ] => destruct x end).
+    simpl. rewrite H, H0. reflexivity.
+  Qed.
+  Next Obligation.
+    split; intros HEq.
+    - repeat (match goal with [ x : halve |- _ ] => destruct x end).
+      apply dist_refl; intros n; apply (HEq (S n)).
+    - intros [| n]; [exact I |]. simpl.
+      repeat (match goal with [ x : halve |- _ ] => destruct x end).
+      revert n; apply dist_refl, HEq.
+  Qed.
+  Next Obligation.
+    intros t1 t2 HEq; destruct n; [exact I |].
+    repeat (match goal with [ x : halve |- _ ] => destruct x end). simpl in *.
+    symmetry; apply HEq.
+  Qed.
+  Next Obligation.
+    intros t1 t2 t3 HEq12 HEq23; destruct n; [exact I |].
+    repeat (match goal with [ x : halve |- _ ] => destruct x end). simpl in *.
+    etransitivity; [apply HEq12 | apply HEq23].
+  Qed.
+  Next Obligation.
+    destruct n; [exact I | ].
+    repeat (match goal with [ x : halve |- _ ] => destruct x end). simpl in *.
+    apply dist_mono, H.
+  Qed.
+
+  Instance halve_chain (σ : chain halve) {σc : cchain σ} : cchain (fun n => unhalved (σ (S n))).
+  Proof.
+    unfold cchain; intros.
+    apply le_n_S in HLei. apply le_n_S in HLej.
+    specialize (chain_cauchy _ σc (S n) (S i) (S j)). simpl. intros Hcauchy.
+    destruct (σ (S i)), (σ (S j)). assumption.
+  Qed.
+
+  Definition compl_halve (σ : chain halve) (σc : cchain σ) : halve :=
+    halved (compl (fun n => unhalved (σ (S n))) (σc := halve_chain σ)).
+
+  Program Definition halve_cm : cmetric halve := mkCMetr compl_halve.
+  Next Obligation.
+    intros [| n]; [exists 0; intros; exact I |].
+    destruct (conv_cauchy _ (σc := halve_chain σ) n) as [m HCon].
+    exists (S m); intros [| i] HLe; [inversion HLe |]. unfold compl_halve.
+    apply le_S_n in HLe.
+    specialize (HCon i _). destruct (σ (S i)). simpl. assumption.
+  Qed.
+
+  Global Instance halve_eq n: Proper (dist (S n) ==> dist n) unhalved.
+  Proof.
+    repeat intro. repeat (match goal with [ x : halve |- _ ] => destruct x end). simpl. assumption.
+  Qed.
+End Halving.
+Arguments halve : clear implicits.
+Ltac unhalve := repeat match goal with
+                       | x: halve _ |- _ => destruct x as [x]
+                       | H: halved _ == halved _ |- _ => simpl in H
+                       | H: halved _ = _ = halved _ |- _ => simpl in H
+                       end.
+
+
 (** Single element space and the distance on it. *)
 Program Instance unit_metric : metric unit :=
   mkMetr (fun _ _ _ => True).
@@ -508,7 +599,7 @@ End ChainApps.
 Section NonexpCMetric.
   Context `{cT : cmetric T} `{cU : cmetric U}.
 
-  (** THe set of non-expansive morphisms between two complete metric spaces is again a complete metric space. *)
+  (** The set of non-expansive morphisms between two complete metric spaces is again a complete metric space. *)
   Global Program Instance nonexp_cmetric : cmetric (T -n> U) | 5 :=
     mkCMetr fun_lub.
   Next Obligation.
diff --git a/lib/ModuRes/MetricRec.v b/lib/ModuRes/MetricRec.v
index c50532751d97ef2c9da60889e76420d03f5f2493..c58873f4c60e2c4e276e0e401fed319e50bb98d6 100644
--- a/lib/ModuRes/MetricRec.v
+++ b/lib/ModuRes/MetricRec.v
@@ -266,7 +266,7 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
       Proof.
         induction k; intros; simpl in *.
         + rewrite DIter_coerce_simpl, tid_left, !tid_right; reflexivity.
-        + rewrite IHk at 1. rewrite <- !tcomp_assoc. clear IHk.
+        + rewrite IHk at 1. rewrite <- 4!tcomp_assoc. clear IHk.
           do 2 (apply equiv_morph; [reflexivity |]).
           rewrite (tow_morphs_coerce _ _ (plus_n_Sm _ _)).
           rewrite <- tcomp_assoc, DIter_coerce_comp.
@@ -279,9 +279,9 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
       Proof.
         induction k; intros; simpl in *.
         + rewrite DIter_coerce_simpl, !tid_right, tid_left; reflexivity.
-        + rewrite (IHk m), !tcomp_assoc; clear IHk.
+        + rewrite (IHk m), 2!tcomp_assoc; clear IHk.
           rewrite (tow_morphsI_coerce _ _ (plus_n_Sm _ _)).
-          rewrite !tcomp_assoc, DIter_coerce_comp.
+          rewrite 3!tcomp_assoc, DIter_coerce_comp.
           rewrite DIter_coerce_simpl, tid_left; reflexivity.
       Qed.
 
@@ -294,7 +294,7 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
         + destruct k; [contradict HEq; omega |].
           assert (HT : k + n = m + n) by omega.
           simpl; rewrite (IHm _ _ HT) at 1; clear IHm.
-          rewrite !tcomp_assoc. apply equiv_morph; [| reflexivity].
+          rewrite 2!tcomp_assoc. apply equiv_morph; [| reflexivity].
           simpl in HEq; generalize HT HEq; rewrite HT; clear HEq HT; intros HEq HT.
           rewrite !DIter_coerce_simpl, tid_left, tid_right; reflexivity.
       Qed.
@@ -308,7 +308,7 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
         + destruct k; [contradict HEq; omega |].
           assert (HT : m + n = k + n) by omega.
           simpl; rewrite (IHm _ _ HT) at 1; clear IHm.
-          rewrite <- !tcomp_assoc. apply equiv_morph; [reflexivity |].
+          rewrite <- 2!tcomp_assoc. apply equiv_morph; [reflexivity |].
           simpl in HEq; generalize HT HEq; rewrite HT; clear HEq HT; intros HEq HT.
           rewrite !DIter_coerce_simpl, tid_left, tid_right; reflexivity.
       Qed.
@@ -321,11 +321,11 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
         + destruct (lt_eq_lt_dec n (S m)) as [ [HLtS | HC ] | HC]; try (contradict HC; omega).
           assert (HEq' : S (m - n) + n = S m - n + n) by omega.
           rewrite (Injection_nm_coerce _ _ _ HEq').
-          simpl; rewrite !tcomp_assoc.
+          simpl; rewrite 3!tcomp_assoc.
           apply equiv_morph; [| reflexivity].
           rewrite (tow_morphs_coerce _ _ (eq_sym (lt_plus_minus HLt))).
           do 2 rewrite <- tcomp_assoc with (f := DIter_coerce _ ∘ tow_morphs _ _).
-          rewrite !DIter_coerce_comp.
+          rewrite 2!DIter_coerce_comp.
           rewrite DIter_coerce_simpl, tid_right, <- tcomp_assoc, @tow_retract, tid_right; reflexivity.
         + destruct (lt_eq_lt_dec n (S m)) as [[HLtS | HC ] | HC]; try (contradict HC; omega).
           subst; assert (HEq : 1 + m = S m - m + m) by omega.
@@ -339,9 +339,9 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
             rewrite tid_left, <- tcomp_assoc, DIter_coerce_comp.
             rewrite DIter_coerce_simpl, tid_right; reflexivity.
           * assert (HEq : n - m + m = S (n - S m) + m) by omega.
-            rewrite (Projection_nm_coerce _ _ _ HEq), Proj_left_comp, <- !tcomp_assoc.
+            rewrite (Projection_nm_coerce _ _ _ HEq), Proj_left_comp, <- 4!tcomp_assoc.
             do 2 (apply equiv_morph; [reflexivity |]).
-            rewrite !DIter_coerce_comp; remember (lt_plus_minus HGtS) as xx.
+            rewrite 2!DIter_coerce_comp; remember (lt_plus_minus HGtS) as xx.
             rewrite (D.UIP _ _ _ xx); reflexivity.
       Qed.
 
@@ -367,14 +367,14 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
         unfold t_nm; destruct (lt_eq_lt_dec n m) as [[HLt | HEq] | HGt].
         + destruct (lt_eq_lt_dec (S n) m) as [[HLtS | HEq] | HC]; try (contradict HC; omega).
           * assert (HEq : S (m - S n) + n = m - n + n) by omega.
-            rewrite (Injection_nm_coerce _ _ _ HEq), Inj_right_comp, !tcomp_assoc.
+            rewrite (Injection_nm_coerce _ _ _ HEq), Inj_right_comp, 3!tcomp_assoc.
             do 2 rewrite <- tcomp_assoc with (g := (Injection_nm _ _)) (h := (tow_morphsI _ _)).
             apply equiv_morph; [| reflexivity].
-            rewrite !DIter_coerce_comp; remember (Logic.eq_sym (lt_plus_minus HLtS)) as xx.
+            rewrite 2!DIter_coerce_comp; remember (Logic.eq_sym (lt_plus_minus HLtS)) as xx.
             rewrite (D.UIP _ _ _ xx); reflexivity.
           * subst; assert (HEq : 1 + n = S n - n + n) by omega.
             rewrite (Injection_nm_coerce _ _ _ HEq); simpl.
-            rewrite tid_right, !tcomp_assoc; apply equiv_morph; [| reflexivity].
+            rewrite tid_right, tcomp_assoc; apply equiv_morph; [| reflexivity].
             rewrite DIter_coerce_comp, !DIter_coerce_simpl; reflexivity.
         + destruct (lt_eq_lt_dec (S n) m) as [[HC | HC] | HGtS]; try (contradict HC; omega).
           subst; rewrite DIter_coerce_simpl; assert (HEq : S m - m + m = 1 + m) by omega.
@@ -385,8 +385,8 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
           assert (HEq : S n - m + m = S (n - m) + m) by omega.
           rewrite (Projection_nm_coerce _ _ _ HEq), <- (tcomp_assoc (Projection_nm _ _)),
           DIter_coerce_comp; simpl.
-          rewrite <- !tcomp_assoc; apply equiv_morph; [reflexivity |].
-          rewrite (tow_morphs_coerce _ _ (lt_plus_minus HGt)), <- !tcomp_assoc.
+          rewrite <- 2!tcomp_assoc; apply equiv_morph; [reflexivity |].
+          rewrite (tow_morphs_coerce _ _ (lt_plus_minus HGt)), <- 2!tcomp_assoc.
           rewrite (tcomp_assoc _ _ (tow_morphsI _ _)), DIter_coerce_comp.
           rewrite DIter_coerce_simpl, tid_left, tow_retract, tid_right; reflexivity.
       Qed.
@@ -566,8 +566,8 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
       rewrite Hk; simpl morph; clear Hk; revert m; rewrite dist_refl.
       unfold chainPE, cutn; rewrite <- tcomp_assoc, coconeCom_l; [apply equiv_morph; [reflexivity |] | omega].
       rewrite t_nmProjection, t_nmEmbedding, <- morph_tnm; simpl.
-      rewrite <- !tcomp_assoc; apply equiv_morph; [reflexivity |].
-      rewrite tcomp_assoc, fmorph_comp, !emp; reflexivity.
+      rewrite <- tcomp_assoc; apply equiv_morph; [reflexivity |].
+      rewrite tcomp_assoc, fmorph_comp, 2!emp; reflexivity.
     Qed.
 
     Lemma CoLimitUnique (C : CoCone DTower) (h : cocone_t _ ECoCone -t> cocone_t _ C)
@@ -600,9 +600,9 @@ Module Solution(Cat : MCat)(M_cat : InputType(Cat)) : SolutionType(Cat)(M_cat).
         rewrite (nonexp_cont2 _ _ _).
         rewrite (umet_complete_ext _ (chainPE _ (AllLimits DTower) DCoCone)), EP_id, tid_left; [reflexivity | intros i; simpl].
         unfold binaryLimit, chainPE; simpl.
-        rewrite !tcomp_assoc, <- (tcomp_assoc (Embeddings i ∘ Projection i)).
+        rewrite 3!tcomp_assoc, <- (tcomp_assoc (Embeddings i ∘ Projection i)).
         simpl; rewrite fmorph_comp.
-        rewrite !retract_EP, fmorph_id, tid_right, <- (tcomp_assoc (Embeddings i)).
+        rewrite 2!retract_EP, fmorph_id, tid_right, <- (tcomp_assoc (Embeddings i)).
         rewrite retract_IP, tid_right; reflexivity.
       + symmetry; apply (colim_unique _ DCoLimit DCoLimit); intros n; rewrite tid_left; reflexivity.
     Qed.
diff --git a/lib/ModuRes/Predom.v b/lib/ModuRes/Predom.v
index 6b12e7737f2edb34a7a2c8f58a54a15a98fdcd12..fe31a3a408640bad19b234e9c8b8c85b88f8ef85 100644
--- a/lib/ModuRes/Predom.v
+++ b/lib/ModuRes/Predom.v
@@ -1,6 +1,5 @@
 Require Import ssreflect.
-Require Export Coq.Program.Program.
-Require Import CSetoid.
+Require Export CSetoid.
 
 Generalizable Variables T U V W.
 
diff --git a/lib/ModuRes/RAConstr.v b/lib/ModuRes/RAConstr.v
index 275b87b85adf80cd6940f3282b352eb5e39325fd..cf1ad43da139e8aa791fe08d3012c084cce0860f 100644
--- a/lib/ModuRes/RAConstr.v
+++ b/lib/ModuRes/RAConstr.v
@@ -1,5 +1,5 @@
 Require Import ssreflect.
-Require Import Predom CSetoid RA.
+Require Import PreoMet RA.
 
 Local Open Scope ra_scope.
 Local Open Scope predom_scope.
@@ -324,6 +324,8 @@ Section Agreement.
 
   Definition ra_ag_inj (t: T): ra_agree := ag_inj t True.
 
+  Local Ltac ra_agree_destr := repeat (match goal with [ x : ra_agree |- _ ] => destruct x end); simpl in *.
+
   Global Instance ra_agree_eq_equiv : Equivalence ra_agree_eq.
   Proof.
     split; intro; intros; destruct x as [tx vx|]; try destruct y as [ty vy|]; try destruct z as [tz vz|]; simpl in *; try (exact I || contradiction); [| |]. (* 3 goals left. *)
@@ -335,19 +337,125 @@ Section Agreement.
   Global Instance ra_agree_res : RA ra_agree.
   Proof.
     split; repeat intro.
-    - repeat (match goal with [ x : ra_agree |- _ ] => destruct x end); simpl in *; try firstorder; [|].
+    - ra_agree_destr; try firstorder; [|].
       + rewrite -H1 H7 H2. reflexivity.
       + rewrite H1 H7 -H2. reflexivity.
-    - repeat (match goal with [ x : ra_agree |- _ ] => destruct x end); simpl in *; try firstorder; [|].
+    - ra_agree_destr; try firstorder; [|].
       + rewrite H1 H3. reflexivity.
       + rewrite -H3 H2. reflexivity.
-    - repeat (match goal with [ x : ra_agree |- _ ] => destruct x end); simpl in *; firstorder.
-    - repeat (match goal with [ x : ra_agree |- _ ] => destruct x end); simpl in *; firstorder.
-    - repeat (match goal with [ x : ra_agree |- _ ] => destruct x end); simpl in *; firstorder.
+    - ra_agree_destr; firstorder.
+    - ra_agree_destr; firstorder.
+    - ra_agree_destr; firstorder.
     - firstorder.
-    - repeat (match goal with [ x : ra_agree |- _ ] => destruct x end); simpl in *; firstorder.
+    - ra_agree_destr; firstorder.
+  Qed.
+
+  (* We also have a metric *)
+  Context {mT: metric T}.
+
+  Definition ra_agree_dist n :=
+    match n with
+    | O => fun _ _ => True
+    | S n => fun x y => match x, y with
+                        | ag_inj t1 v1, ag_inj t2 v2 => v1 == v2 /\ (v1 -> t1 = S n = t2)
+                        | ag_unit, ag_unit => True
+                        | _, _ => False
+                        end
+    end.
+
+  Global Program Instance ra_agree_metric : metric ra_agree := mkMetr ra_agree_dist.
+  Next Obligation.
+    repeat intro. destruct n as [|n]; first by auto.
+    ra_agree_destr; try firstorder.
+    - rewrite -H1 -H2. assumption.
+    - rewrite H1 H2. assumption.
+  Qed.
+  Next Obligation.
+    repeat intro. split.
+    - intros Hall. ra_agree_destr; last exact I; try (specialize (Hall (S O)); now firstorder); [].
+      split.
+      + specialize (Hall (S O)); now firstorder.
+      + intro. eapply dist_refl. intro. specialize (Hall n). destruct n as [|n]; first by apply: dist_bound.
+        firstorder.
+    - repeat intro. destruct n as [|n]; first by auto. ra_agree_destr; try firstorder.
+      + rewrite H0. reflexivity.
+  Qed.
+  Next Obligation.
+    repeat intro. destruct n as [|n]; first by auto.
+    ra_agree_destr; try firstorder.
+  Qed.
+  Next Obligation.
+    repeat intro. destruct n as [|n]; first by auto.
+    ra_agree_destr; try firstorder; [].
+    rewrite H1 -H2. reflexivity.
+  Qed.
+  Next Obligation.
+    repeat intro. destruct n as [|n]; first by auto.
+    ra_agree_destr; try firstorder; [].
+    eapply dist_mono. assumption.
   Qed.
 
+  (* And a complete metric! *)
+  Context {cmT: cmetric T}.
+
+  Program Definition unInj (σ : chain ra_agree) {σc : cchain σ} (HNE : σ (S O) <> ag_unit) : chain T :=
+    fun i => match σ (S i) with
+             | ag_unit => False_rect _ _
+             | ag_inj t v => t
+             end.
+  Next Obligation.
+    specialize (σc (S O) (S O) (S i)); rewrite <- Heq_anonymous in σc.
+    destruct (σ (S O)) as [ t v |]; last (contradiction HNE; reflexivity).
+    apply σc; omega.
+  Qed.
+
+  Instance unInj_c (σ : chain ra_agree) {σc : cchain σ} HNE : cchain (unInj σ HNE).
+  Proof.
+    (* This does NOT hold!
+    intros [| k] n m HLE1 HLE2; [apply dist_bound |]; unfold unSome.
+    generalize (@eq_refl _ (σ (S n))); pattern (σ (S n)) at 1 3.
+    destruct (σ (S n)) as [v |]; simpl; intros EQn.
+    - generalize (@eq_refl _ (σ (S m))); pattern (σ (S m)) at 1 3.
+      destruct (σ (S m)) as [v' |]; simpl; intros EQm.
+      + specialize (σc (S k) (S n) (S m)); rewrite <- EQm, <- EQn in σc.
+        apply σc; auto with arith.
+      + exfalso; specialize (σc 1 1 (S m)); rewrite <- EQm in σc.
+        destruct (σ 1) as [v' |]; [contradiction σc; auto with arith | contradiction HNE; reflexivity].
+    - exfalso; specialize (σc 1 1 (S n)); rewrite <- EQn in σc.
+      destruct (σ 1) as [v |]; [contradiction σc; auto with arith | contradiction HNE; reflexivity].*)
+  Admitted.
+
+  Program Definition option_compl (σ : chain ra_agree) {σc : cchain σ} :=
+    match σ (S O) with
+      | ag_unit => ag_unit
+      | ag_inj t v => ag_inj (compl (unInj σ _)) v
+    end.
+
+  (*
+  Global Program Instance option_cmt : cmetric (option T) := 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.
+    - assert (HT := conv_cauchy (unSome σ (option_compl_obligation_1 _ _ _ EQ1)) (S n)).
+      destruct HT as [k HT]; exists (max k (S n)); intros.
+      destruct (σ i) as [vi |] eqn: EQi; [unfold dist; simpl; rewrite (HT i) by eauto with arith | exfalso].
+      + unfold unSome; generalize (@eq_refl _ (σ (S i))); pattern (σ (S i)) at 1 3.
+        destruct (σ (S i)) as [vsi |]; intros EQsi; clear HT; [| exfalso].
+        * assert (HT : S n <= i) by eauto with arith.
+          specialize (σc (S n) (S i) i); rewrite EQi, <- EQsi in σc.
+          apply σc; auto with arith.
+        * specialize (σc 1 1 (S i)); rewrite <- EQ1, <- EQsi in σc.
+          apply σc; auto with arith.
+      + clear HT; specialize (σc 1 1 i); rewrite <- EQ1, EQi in σc.
+        apply σc; auto with arith.
+        rewrite <- HLe, <- Max.le_max_r; auto with arith.
+    - exists 1; intros.
+      destruct (σ i) as [vi |] eqn: EQi; [| reflexivity].
+      specialize (σc 1 1 i); rewrite <- EQ1, EQi in σc.
+      apply σc; auto with arith.
+  Qed.*)
+    
+
 End Agreement.
 
 
diff --git a/world_prop.v b/world_prop.v
index 8f9f229218ea5b816e1d863db6ecd2e85534576c..07bd21a4624182080d86dc65f8330c0fee81333c 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -1,13 +1,15 @@
 (** 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 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 *)
 Module Type WORLD_PROP (Res : RA_T).
   (* PreProp: The solution to the recursive equation. Equipped with a discrete order. *)
-  Parameter PreProp    : cmtyp.
+  Parameter PreProp    : Type.
+  Declare Instance PProp_t  : Setoid PreProp.
+  Declare Instance PProp_m  : metric PreProp.
+  Declare Instance PProp_cm : cmetric PreProp.
   Instance PProp_preo  : preoType PreProp   := disc_preo PreProp.
   Instance PProp_pcm   : pcmType PreProp    := disc_pcm PreProp.
   Instance PProp_ext   : extensible PreProp := disc_ext PreProp.
@@ -17,16 +19,15 @@ Module Type WORLD_PROP (Res : RA_T).
   Definition Props     := Wld -m> UPred (Res.res).
 
   (* Define all the things on Props, so they have names - this shortens the terms later. *)
-  (* TODO: Why again does this not use priority 0? *)
-  Instance Props_ty   : Setoid Props  | 1 := _.
-  Instance Props_m    : metric Props  | 1 := _.
-  Instance Props_cm   : cmetric Props | 1 := _.
-  Instance Props_preo : preoType Props| 1 := _.
-  Instance Props_pcm  : pcmType Props | 1 := _.
+  Instance Props_ty   : Setoid Props  | 0 := _.
+  Instance Props_m    : metric Props  | 0 := _.
+  Instance Props_cm   : cmetric Props | 0 := _.
+  Instance Props_preo : preoType Props| 0 := _.
+  Instance Props_pcm  : pcmType Props | 0 := _.
 
   (* Establish the recursion isomorphism *)
-  Parameter ı  : PreProp -n> halve (cmfromType Props).
-  Parameter ı' : halve (cmfromType Props) -n> PreProp.
+  Parameter ı  : PreProp -n> halve Props.
+  Parameter ı' : halve Props -n> PreProp.
   Axiom iso : forall P, ı' (ı P) == P.
   Axiom isoR: forall T, ı (ı' T) == T.
 End WORLD_PROP.
diff --git a/world_prop_recdom.v b/world_prop_recdom.v
index 36764a1df0148bf48a8f22d3e65dc26495c4d945..11271b1bb15f1fab804df08f8ccce6b67f9ec50c 100644
--- a/world_prop_recdom.v
+++ b/world_prop_recdom.v
@@ -63,16 +63,17 @@ Module WorldProp (Res : RA_T) : WORLD_PROP Res.
       the space of worlds. We'll store the actual solutions in the
       worlds, and use the action of the FPropO on them as the space we
       normally work with. *)
-  Definition PreProp := DInfO.
-  Definition Props   := FProp PreProp.
-  Definition Wld     := (nat -f> PreProp).
-
-  (* Define an order on PreProp. *)
+  Definition PreProp : Type := DInfO.
+  Instance PProp_t  : Setoid PreProp := _.
+  Instance PProp_m  : metric PreProp := _.
+  Instance PProp_cm : cmetric PreProp := _.
   Instance PProp_preo: preoType PreProp   := disc_preo PreProp.
   Instance PProp_pcm : pcmType PreProp    := disc_pcm PreProp.
   Instance PProp_ext : extensible PreProp := disc_ext PreProp.
 
-  (* Give names to the things for Props, so the terms can get shorter. *)
+  (* Define worlds and propositions *)
+  Definition Wld     := (nat -f> PreProp).
+  Definition Props   := FProp PreProp.
   Instance Props_ty   : Setoid Props     := _.
   Instance Props_m    : metric Props     := _.
   Instance Props_cm   : cmetric Props    := _.
@@ -80,8 +81,8 @@ Module WorldProp (Res : RA_T) : WORLD_PROP Res.
   Instance Props_pcm  : pcmType Props    := _.
 
   (* Establish the isomorphism *)
-  Definition ı  : PreProp -t> halve (cmfromType Props) := Unfold.
-  Definition ı' : halve (cmfromType Props) -t> PreProp := Fold.
+  Definition ı  : DInfO -t> halveCM (cmfromType Props) := Unfold.
+  Definition ı' : halveCM (cmfromType Props) -t> DInfO := Fold.
 
   Lemma iso P : ı' (ı P) == P.
   Proof. apply (FU_id P). Qed.