diff --git a/iris_derived_rules.v b/iris_derived_rules.v
index 51a519b725c67050881a496cc746b7d921a4df78..404b686abae1ec25550c85165790ecc519856d65 100644
--- a/iris_derived_rules.v
+++ b/iris_derived_rules.v
@@ -1,4 +1,4 @@
-Require Import ssreflect.
+Require Import Ssreflect.ssreflect.
 Require Import world_prop core_lang lang iris_core iris_plog iris_vs_rules iris_ht_rules.
 Require Import ModuRes.RA ModuRes.SPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap ModuRes.CMRA ModuRes.DecEnsemble.
 
diff --git a/iris_plog.v b/iris_plog.v
index 6d60d1141fdd364b2d928823da95a05938aec9de..3f51b3869109cb94ec9862be320f7daf16c8c8e9 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -248,7 +248,8 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
                    exists w', P w' (S (S k))
                               /\ wsat σ (m2 ∪ mf) (w' · wf) (S (S k)))].
     Next Obligation.
-      inversion HLe.
+      repeat intro.
+      by inversion HLe.
     Qed.
     Next Obligation.
       intros n1 n2 HLe HP wf; intros.
diff --git a/iris_vs_rules.v b/iris_vs_rules.v
index 9920535f7b1db96d2194f9c9bb2fcf23b68d602f..9c4b024bdfbb85112c5c06f6fa9f55532089cafa 100644
--- a/iris_vs_rules.v
+++ b/iris_vs_rules.v
@@ -165,7 +165,7 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
       - exists (w2, wq). split; last split.
         + rewrite [ra_op]lock. simpl. reflexivity.
         + assumption.
-        + apply propsMN, HQ. omega.
+        + eapply propsMN, HQ. omega.
       - now rewrite -assoc.
     Qed.
 
diff --git a/lib/ModuRes/Finmap.v b/lib/ModuRes/Finmap.v
index 337ab76549977e67b18b07efe0f3a57c9414f8b7..f2b2282d004d2acdae496f297a91ea02530546ea 100644
--- a/lib/ModuRes/Finmap.v
+++ b/lib/ModuRes/Finmap.v
@@ -1,8 +1,8 @@
-Require Import ssreflect.
+Require Import Ssreflect.ssreflect Omega.
+Require Import Arith Min Max List ListSet Lists.
 Require Import MetricCore.
 Require Import PreoMet.
 Require Import RA CMRA SPred.
-Require Import Arith Min Max List ListSet Lists.
 
 Set Bullet Behavior "Strict Subproofs".
 
@@ -548,11 +548,11 @@ Section FinDom.
         refine (fix F (l: list K) :=
                   match l as l return (forall f, dom f = l -> T f) with
                   | [] => fun f Hdom => Text fdEmpty f _ Temp
-                  | k::l => fun f Hdom => let f' := f \ k in
-                                          let Hindom: k ∈ dom f := _ in
-                                          let v' := fdLookup_indom f k Hindom in
-                                          Text (fdStrongUpdate k (Some v') f') f _
-                                               (Tstep k v' f' _ (F l f' _))
+                  | k::l' => fun f Hdom => let f' := f \ k in
+                                           let Hindom: k ∈ dom f := _ in
+                                           let v' := fdLookup_indom f k Hindom in
+                                           Text (fdStrongUpdate k (Some v') f') f _
+                                                (Tstep k v' f' _ (F l' f' _))
                   end); clear F.
         - split.
           + move=>k /=. symmetry. apply fdLookup_notin_strong. rewrite Hdom. tauto.
@@ -566,7 +566,7 @@ Section FinDom.
           + rewrite Hdom /dom /=. f_equal. rewrite /dom /= Hdom.
             rewrite DecEq_refl.
             assert (Hnod := dom_nodup f). rewrite Hdom in Hnod.
-            assert (Hfilt1: (filter_dupes [] l0) = l0).
+            assert (Hfilt1: (filter_dupes [] l') = l').
             { apply filter_dupes_id. simpl. inversion Hnod; subst. assumption. }
             rewrite Hfilt1. apply filter_dupes_id. assumption.
         - subst f'. apply fdLookup_notin. rewrite fdStrongUpdate_eq. reflexivity.
@@ -581,20 +581,6 @@ Section FinDom.
         fun f => fdRectInner (dom f) f eq_refl.
     End Recursion.
 
-    (* No need to restrict this Lemma to fdRectInner - that just messes up the details. *)
-(*    Lemma fdRectInner_eqL l l' f (Heq: dom f = l) (Heq': dom f = l')
-          (T: (K -f> V) -> Type) (F: forall l (f: K -f> V), dom f = l -> T f) :
-      F l f Heq = F l' f Heq'.
-    Proof.
-      assert (Heql: l = l').
-      { transitivity (dom f); first symmetry; assumption. }
-      revert Heq'.
-      refine (match Heql in eq _ l'' return (forall Heq' : dom f = l'', F l f Heq = F l'' f Heq') with
-              | eq_refl => _
-              end).
-      move=>Heq'. reflexivity.
-    Qed. *)
-
     Section Fold.
       Context {T: Type}.
       Context (Temp: T) (Tstep: K -> V -> T -> T).
diff --git a/lib/ModuRes/Util.v b/lib/ModuRes/Util.v
index 43eb10cdc6daa9af4960b2192ab0c76fee8ff245..8de64a13952ab45723105f7db19844556e8ef027 100644
--- a/lib/ModuRes/Util.v
+++ b/lib/ModuRes/Util.v
@@ -71,5 +71,3 @@ Ltac contradiction_eq := match goal with
 
 (* Well-founded induction. *)
 Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
-  
\ No newline at end of file