diff --git a/iris_core.v b/iris_core.v
index b6835b6b4eb983e988550af32874009ba01799d7..743d66ba208ff8a2e8b03acb2b1b7771434741a4 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -139,24 +139,22 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       intros n1 n2 _ _ HLe _; apply mono_dist; omega.
     Qed.
 
-    Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).
-
-    Instance intEq_equiv : Proper (equiv ==> equiv ==> equiv) intEqP.
+    Instance subrel_dist_n `{mT : metric T} (n m: nat) (Hlt: m < n) : subrelation (dist n) (dist m).
     Proof.
-      intros l1 l2 EQl r1 r2 EQr n r.
-      split; intros HEq; do 2 red.
-      - rewrite <- EQl, <- EQr; assumption.
-      - rewrite ->EQl, EQr; assumption.
+      intros x y HEq. eapply mono_dist, HEq. omega.
     Qed.
 
-    Instance intEq_dist n : Proper (dist n ==> dist n ==> dist n) intEqP.
-    Proof.
-      intros l1 l2 EQl r1 r2 EQr m r HLt.
-      split; intros HEq; do 2 red.
-      - etransitivity; [| etransitivity; [apply HEq |] ];
-        apply mono_dist with n; eassumption || now auto with arith.
-      - etransitivity; [| etransitivity; [apply HEq |] ];
-        apply mono_dist with n; eassumption || now auto with arith.
+    Program Definition intEq: T -n> T -n> Props :=
+      n[(fun t1 => n[(fun t2 => pcmconst (intEqP t1 t2))])].
+    Next Obligation.
+      intros t2 t2' Heqt2. intros w m r HLt.
+      change ((t1 = S m = t2) <-> (t1 = S m = t2')). (* Why, oh why... *)
+      split; (etransitivity; [eassumption|]); eapply mono_dist; (eassumption || symmetry; eassumption).
+    Qed.
+    Next Obligation.
+      intros t1 t1' Heqt1. intros t2 w m r HLt.
+      change ((t1 = S m = t2) <-> (t1' = S m = t2)). (* Why, oh why... *)
+      split; (etransitivity; [|eassumption]); eapply mono_dist; (eassumption || symmetry; eassumption).
     Qed.
 
   End IntEq.
diff --git a/iris_plog.v b/iris_plog.v
index b6f23949b53f6ccd31486d5c93842a9f6958726c..1f9118f2e0f8e7d7af5dfd26c8c95444ecf7a477 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -25,25 +25,28 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
     (** Invariants **)
     Definition invP i P w : UPred pres :=
-      intEqP (w i) (Some (ı' P)).
+      intEq (w i) (Some (ı' P)) w.
     Program Definition inv i : Props -n> Props :=
       n[(fun P => m[(invP i P)])].
     Next Obligation.
-      intros w1 w2 EQw; unfold invP; simpl morph.
+      intros w1 w2 EQw; unfold invP.
       destruct n; [apply dist_bound |].
-      apply intEq_dist; [apply EQw | reflexivity].
+      rewrite (EQw i).
+      now eapply met_morph_nonexp.
     Qed.
     Next Obligation.
-      intros w1 w2 Sw; unfold invP; simpl morph.
-      intros n r HP; do 2 red; specialize (Sw i); do 2 red in HP.
+      intros w1 w2 Sw; unfold invP.
+      intros n r HP; specialize (Sw i).
       destruct (w1 i) as [μ1 |]; [| contradiction].
-      destruct (w2 i) as [μ2 |]; [| contradiction]; simpl in Sw.
+      destruct (w2 i) as [μ2 |]; [| contradiction]. simpl in Sw.
       rewrite <- Sw; assumption.
     Qed.
     Next Obligation.
-      intros p1 p2 EQp w; unfold invP; simpl morph.
-      apply intEq_dist; [reflexivity |].
-      apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
+      intros p1 p2 EQp w; unfold invP.
+      cut ((w i === Some (ı' p1)) = n = (w i === Some (ı' p2))).
+      { intros Heq. now eapply Heq. }
+      eapply met_morph_nonexp.
+      now eapply dist_mono, (met_morph_nonexp _ _ ı').
     Qed.
 
   End Invariants.
diff --git a/lib/ModuRes/MetricCore.v b/lib/ModuRes/MetricCore.v
index ecb555cbc53b71ab87a4f9e253ca47adc99767ce..210bf9156d090604684bb44c2cd67d2ca87e4eab 100644
--- a/lib/ModuRes/MetricCore.v
+++ b/lib/ModuRes/MetricCore.v
@@ -37,6 +37,15 @@ Record Mtyp :=
 Instance mtyp_proj_metr {M : Mtyp} : metric M := mmetr M.
 Definition mfromType (T : Type) `{mT : metric T} := Build_Mtyp (fromType T) _.
 
+(* And now it gets annoying that we are not fully unbundled... *)
+Global Instance metric_dist_equiv (T: Type) `{mT: metric T} n: Equivalence (dist n).
+Proof.
+  split.
+  - intros x. eapply dist_refl. reflexivity.
+  - now eapply dist_sym.
+  - now eapply dist_trans.
+Qed.
+
 Section DistProps.
   Context `{mT : metric T}.
 
@@ -193,6 +202,12 @@ Arguments mkUMorph [T U eqT mT eqT0 mU] _ _.
 Arguments met_morph [T U] {eqT mT eqT0 mU} _.
 Infix "-n>" := metric_morphism (at level 45, right associativity).
 
+Global Instance metric_morphism_proper T U `{mT : metric T} `{mU : metric U} n (f: T -n> U):
+  Proper (dist n ==> dist n) f.
+Proof.
+  now eapply met_morph_nonexp.
+Qed.
+
 Program Definition mkNMorph T U `{mT : metric T} `{mU : metric U} (f: T -> U)
         (NEXP : forall n, Proper (dist n ==> dist n) f) :=
   mkUMorph s[(f)] _.
@@ -204,7 +219,7 @@ Qed.
 Arguments mkNMorph [T U eqT mT eqT0 mU] _ _.
 Notation "'n[(' f ')]'" := (mkNMorph f _).
 
-Instance subrel_dist `{mT : metric T} n : subrelation equiv (dist n).
+Instance subrel_dist `{mT : metric T} n : subrelation equiv (dist n) | 5.
 Proof.
   intros x y HEq; revert n; rewrite dist_refl; assumption.
 Qed.
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 74b939e96f3737eeb0859354ea0836b018848e7b..695fe2139e6aaea467aba5a4950cd7a37f0808b4 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -391,7 +391,7 @@ Section InfiniteProduct.
   Global Instance ra_equiv_infprod : Equivalence ra_eq_infprod.
   Proof. split; repeat intro; [ | rewrite (H i) | rewrite (H i), (H0 i) ]; reflexivity. Qed.
   
-  Global Instance ra_type_infprod : Setoid ra_res_infprod := mkType ra_eq_infprod.
+  Global Instance ra_type_infprod : Setoid ra_res_infprod | 5 := mkType ra_eq_infprod.
   Global Instance ra_unit_infprod : RA_unit _ := fun i => ra_unit (S i).
   Global Instance ra_op_infprod : RA_op _ := fun f g i => f i · g i.
   Global Instance ra_valid_infprod : RA_valid _ := fun f => forall i, ra_valid (f i).