diff --git a/iris_meta.v b/iris_meta.v
index e43cfe7a41f8921c849ff0327f65fb3d9b2cd664..c8d91366e8e585cf311f68cdd7f9a26500cd3156 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -184,7 +184,7 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
       n[(fun v => pcmconst (sp_const (Q v)))].
     Next Obligation.
       move=>v1 v2 EQv. destruct n; first exact:dist_bound.
-      intros w m Hlt. rewrite /= /sp_constF. destruct m; first reflexivity.
+      intros w m Hlt. rewrite /=. destruct m; first reflexivity.
       rewrite EQv. reflexivity.
     Qed.
 
@@ -379,7 +379,7 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
         apply top_valid. apply htValid. rewrite sc_top_unit.
         (* Now fall back to proving this in the model. *)
         move=>w n. destruct n; first (intro;exact:bpred).
-        rewrite /= /sp_constF. move=>[[Hφ Hval] HownS].
+        rewrite /=. move=>[[Hφ Hval] HownS].
         eapply wpValue; [].
         simpl. exists σ'. split; assumption.
     Grab Existential Variables.
diff --git a/iris_plog.v b/iris_plog.v
index 7dc8d6a247e524099b8b70b8305e1633483a3aa5..e5e3f54872e2816a548e75f1a223237a8016e2df 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -118,11 +118,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
       rewrite comm -comp_finmap_move comm ra_op_unit. reflexivity.
     Qed.
 
-    (* Go through some struggle to even write down world satisfaction... *)
-    (*
-    Local Open Scope finmap_scope.
-    *)
-    
+    (** Now we define world satisfaction **)
     Lemma world_inv_val {wt n}:
       forall (pv: cmra_valid wt n) {i agP} (Heq: (Invs wt) i = n = Some agP), cmra_valid agP n.
     Proof.
@@ -191,16 +187,13 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
     Qed.  
 
     (* It may be possible to use "later_sp" here, but let's avoid indirections where possible. *)
-    Definition wsatF σ m w n :=
-      match n with
-      | S (S n') => exists s : nat -f> Wld,
-                               let wt := comp_finmap w s in
-                               wsatTotal (S n') σ s m wt
-      | _        => True
-      end.
-
     Program Definition wsat σ m w : SPred :=
-      p[(wsatF σ m w)].
+      p[(fun n => match n return _ with
+                  | S (S n') => exists s : nat -f> Wld,
+                                           let wt := comp_finmap w s in
+                                           wsatTotal (S n') σ s m wt
+                  | _        => True
+                  end)].
     Next Obligation.
       intros n1 n2 HLe. do 2 (destruct n2; first (intro; exact I)).
       do 2 (destruct n1; first (exfalso; omega)).
diff --git a/lib/ModuRes/Agreement.v b/lib/ModuRes/Agreement.v
index f7d0375dce2ee82420bb3e2bd622d0d311c7410e..8dae4ac6f04d7099eb608c2947e0bdcf34dae355 100644
--- a/lib/ModuRes/Agreement.v
+++ b/lib/ModuRes/Agreement.v
@@ -301,19 +301,14 @@ Section Agreement.
     move=><-. assumption.
   Qed.
 
-  Definition ra_ag_tsdiag_n (σ : chain ra_agree) n: T :=
-    match σ n with
-    | ag_inj v' ts' tsx' => ts' n
-    end.
-
   Program Definition ra_ag_compl (σ : chain ra_agree) {σc : cchain σ} :=
     ag_inj (compl (ra_ag_vchain σ))
-           (fun n => ra_ag_tsdiag_n σ n) _.
+           (fun n => match σ n return _ with
+                     | ag_inj v' ts' tsx' => ts' n end) _.
   Next Obligation.
     move=>n i HLe pv. simpl. rewrite -/dist.    
     assert (pvc: compl (ra_ag_vchain σ) i) by assumption.
     destruct n as [|n]; first by apply: dist_bound.
-    unfold ra_ag_tsdiag_n.
     ddes (σ i) at 1 3 as [vi tsi tsxi] deqn:EQi.
     ddes (σ (S n)) at 1 3 as [vSn tsSn tsxSn] deqn:EQSn.
     cchain_eleq σ at i (S n) lvl:(S n); move=>[EQv EQts].
@@ -336,7 +331,6 @@ Section Agreement.
       inversion EQi; subst. reflexivity.
     - move=>j HLej pv1.
       destruct j as [|j]; first by apply: dist_bound.
-      unfold ra_ag_tsdiag_n.
       rewrite /ra_ag_vchain /= in pv1. move:pv1.
       ddes (σ (S j)) at 1 3 6 as [vSSj tsSSj tsxSSj] deqn:EQSSj.
       intros pv1. cchain_eleq σ at (S j) i lvl:(S j); move=>[EQv EQts].
@@ -347,15 +341,6 @@ Section Agreement.
   Global Instance ra_ag_pcm: pcmType ra_agree.
   Proof.
     split. repeat intro. eapply ra_ag_pord. unfold compl, ra_ag_cmt, ra_ag_compl.
-    assert (HT: forall n, ra_ag_vchain ρ n n -> ra_ag_tsdiag_n σ n = n = ra_ag_tsdiag_n ρ n).
-    { move=>n pv. destruct n as [|n]; first by apply: dist_bound.
-      unfold ra_ag_tsdiag_n.
-      ddes (σ (S n)) at 1 3 as [vσn tsσn tsxσn] deqn:EQσn.
-      ddes (ρ (S n)) at 1 3 as [vρn tsρn tsxρn] deqn:EQρn.
-      specialize (H (S n)). rewrite ->ra_ag_pord in H.
-      rewrite <-EQσn, <-EQρn, comm in H. destruct H as [EQv EQts].
-      apply EQts. rewrite EQv. rewrite /ra_ag_vchain -EQρn in pv. assumption.
-    }
     split.
     - move=>n. split; first by (intros (pv1 & pv2 & _); tauto).
       simpl. move=>pv. move:(pv). rewrite {1}/ra_ag_vchain. simpl.
@@ -366,7 +351,12 @@ Section Agreement.
         ddes (σ n) at 1 3 as [vσn tsσn tsxσn] deqn:EQσn.
         specialize (H n). rewrite ->ra_ag_pord, <-EQρn, <-EQσn, comm in H.
         destruct H as [EQv _]. rewrite <-EQv in pvρ. destruct pvρ as [pv1 _]. assumption. }
-      do 2 (split; first assumption). symmetry. apply HT. assumption.
+      do 2 (split; first assumption). symmetry.
+      destruct n as [|n]; first by apply: dist_bound.
+      rewrite -EQρn. destruct (σ (S n)) as [vσn tsσn rsxσn] eqn:EQσn.
+      specialize (H (S n)). rewrite ->ra_ag_pord in H.
+      rewrite ->EQσn, <-EQρn, comm in H. destruct H as [EQv EQts].
+      apply EQts. rewrite EQv. rewrite /ra_ag_vchain -EQρn in pv. assumption.
     - intros n (pv1 & pv2 & EQ). reflexivity.
   Qed.
 
diff --git a/lib/ModuRes/Finmap.v b/lib/ModuRes/Finmap.v
index c5da2f2cc80c79f7a1bd055c41051606484f29b6..7215550b57d84810642947250dd1252b6f1d7f8d 100644
--- a/lib/ModuRes/Finmap.v
+++ b/lib/ModuRes/Finmap.v
@@ -552,39 +552,46 @@ Section FinDom2.
               (Temp: T fdEmpty).
       Context (Tstep: forall (k:K) (v:V) (f: K -f> V), ~(k ∈ dom f) -> T f -> T (f + [fd k <- v ] )).
 
-      Definition fdRectInner: forall l f, dom f = l -> T f.
-      Proof.
-        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 (f' + [fd k <- v' ]) f _
-                                                (Tstep k v' f' _ (F l' f' _))
-                  end); clear F.
-        - split.
-          + move=>k /=. symmetry. apply fdLookup_notin_strong. rewrite Hdom. tauto.
-          + rewrite Hdom. reflexivity.
-        - rewrite Hdom. left. reflexivity.
-        - subst f'. split.
-          + move=>k'. destruct (dec_eq k k') as [EQ|NEQ].
-            * subst k'. rewrite fdStrongUpdate_eq. subst v'. symmetry. eapply fdLookup_indom_corr.
-              reflexivity.
-            * erewrite !fdStrongUpdate_neq by assumption. reflexivity.
-          + rewrite Hdom /dom /=. f_equal. rewrite /dom /= Hdom.
-            rewrite DecEq_refl.
-            assert (Hnod := dom_nodup f). rewrite Hdom in Hnod.
-            assert (Hfilt1: (filter_dupes ([])%list 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.
-        - subst f'. rewrite /dom /fdStrongUpdate /=.
-          rewrite Hdom. destruct (dec_eq k k) as [_|NEQ]; last (exfalso; now apply NEQ).
-          apply filter_dupes_id with (dupes:=[]); simpl.
-          assert (Hno:= dom_nodup f). rewrite Hdom in Hno.
-          inversion Hno; subst. assumption.
-      Defined.
+      Program Fixpoint fdRectInner l: forall f, dom f = l -> T f :=
+        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 (f' + [fd k <- v' ]) f _
+                                      (Tstep k v' f' _ (fdRectInner l' f' _))
+        end.
+      Next Obligation.
+        split.
+        - move=>k /=. symmetry. apply fdLookup_notin_strong. rewrite Hdom. tauto.
+        - rewrite Hdom. reflexivity.
+      Qed.
+      Next Obligation.
+        rewrite Hdom. left. reflexivity.
+      Qed.
+      Next Obligation.
+        split.
+        - move=>k'. destruct (dec_eq k k') as [EQ|NEQ].
+          + subst k'. rewrite fdStrongUpdate_eq. symmetry. eapply fdLookup_indom_corr.
+            reflexivity.
+          + erewrite !fdStrongUpdate_neq by assumption. reflexivity.
+        - rewrite Hdom /dom /=. f_equal. rewrite /dom /= Hdom.
+          rewrite DecEq_refl.
+          assert (Hnod := dom_nodup f). rewrite Hdom in Hnod.
+          assert (Hfilt1: (filter_dupes ([])%list l') = l').
+          { apply filter_dupes_id. simpl. inversion Hnod; subst. assumption. }
+          rewrite Hfilt1. apply filter_dupes_id. assumption.
+      Qed.
+      Next Obligation.
+        apply fdLookup_notin. rewrite fdStrongUpdate_eq. reflexivity.
+      Qed.
+      Next Obligation.
+        rewrite /dom /fdStrongUpdate /=.
+        rewrite Hdom. destruct (dec_eq k k) as [_|NEQ]; last (exfalso; now apply NEQ).
+        apply filter_dupes_id with (dupes:=[]); simpl.
+        assert (Hno:= dom_nodup f). rewrite Hdom in Hno.
+        inversion Hno; subst. assumption.
+      Qed.
 
       Definition fdRect: forall f, T f :=
         fun f => fdRectInner (dom f) f eq_refl.
diff --git a/lib/ModuRes/SPred.v b/lib/ModuRes/SPred.v
index e8dcc2fdbf486aec5190e077a434e5623dd9f389..b0a3fd28d9d1dcb53b9d8c2ff5df239de6a2d3ef 100644
--- a/lib/ModuRes/SPred.v
+++ b/lib/ModuRes/SPred.v
@@ -16,13 +16,10 @@ Arguments mkSPred _ _ _.
 Notation "'p[(' f ')]'" := (mkSPred f _ _).
 
 Section Props.
-  Definition sp_constF (P: Prop) :=
-    fun n => match n with
-             | O => True
-             | S _ => P end.
-  Global Arguments sp_constF _ !n /.
   Program Definition sp_const P :=
-    p[(sp_constF P)].
+    p[(fun n => match n return _ with
+                | O => True
+                | S _ => P end)].
   Next Obligation.
     move=>n m Hle. destruct m, n; simpl; tauto || inversion Hle.
   Qed.