diff --git a/README b/README
index 5e2238711d1f93de35605c189b0b650ca8b76f22..53ccfc1bb8d08577edb61b5243af406f8a5acae1 100644
--- a/README
+++ b/README
@@ -7,10 +7,11 @@ This version is known to compile with:
  - Ssreflect 1.6
  - Autosubst 1.4
 
-For development, better make sure you have a version of Ssreflect that includes commit be724937
-(no such version has been released so far, you'll have to fetch the development branch yourself).
-Iris compiles fine even without this patch, but proof bullets will only be in 'strict' (enforcing)
-mode with the fixed version of Ssreflect.
+For development, better make sure you have a version of Ssreflect that includes
+commit be724937 (no such version has been released so far, you will have to
+fetch the development branch yourself). Iris compiles fine even without this
+patch, but proof bullets will only be in 'strict' (enforcing) mode with the
+fixed version of Ssreflect.
  
 BUILDING INSTRUCTIONS
 ---------------------
diff --git a/_CoqProject b/_CoqProject
index 39a1644d83ddf7e0137f2869f919ea58c0f81a72..3eaad988924579c1a6a25342e10d2a6cc295a063 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -36,6 +36,8 @@ prelude/list.v
 prelude/error.v
 modures/option.v
 modures/cmra.v
+modures/cmra_big_op.v
+modures/cmra_tactics.v
 modures/sts.v
 modures/auth.v
 modures/fin_maps.v
@@ -45,7 +47,6 @@ modures/base.v
 modures/dra.v
 modures/cofe_solver.v
 modures/agree.v
-modures/ra.v
 modures/excl.v
 iris/model.v
 iris/adequacy.v
@@ -56,14 +57,13 @@ iris/viewshifts.v
 iris/wsat.v
 iris/ownership.v
 iris/weakestpre.v
-iris/language.v
 iris/pviewshifts.v
 iris/resources.v
 iris/hoare.v
-iris/parameter.v
+iris/language.v
+iris/functor.v
 iris/tests.v
 barrier/heap_lang.v
-barrier/parameter.v
 barrier/lifting.v
 barrier/sugar.v
 barrier/tests.v
diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index 2d683c1f48a12873f43fa76366f2b6965b295c8c..f58ee88c04e71f01a659eeac16fe068d853c564b 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -390,8 +390,10 @@ Section Language.
   Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
     ∃ K e1' e2', e1 = fill K e1' ∧ e2 = fill K e2' ∧
                  prim_step e1' σ1 e2' σ2 ef.
-
-  Global Program Instance heap_lang : Language expr value state := {|
+  Program Canonical Structure heap_lang : language := {|
+    language.expr := expr;
+    language.val := value;
+    language.state := state;
     of_val := v2e;
     to_val := e2v;
     language.atomic := atomic;
diff --git a/barrier/lifting.v b/barrier/lifting.v
index 5ecfc3151f2dffb5451a4db96876dfa617e7bbe6..704c29a9a4a753e1e71522a9009dd901ca1e0b18 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -1,15 +1,16 @@
 Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre barrier.parameter.
+Require Export iris.weakestpre barrier.heap_lang.
 Import uPred.
 
-(* TODO RJ: Figure out a way to to always use our Σ. *)
+Section lifting.
+Context {Σ : iFunctor}.
+Implicit Types P : iProp heap_lang Σ.
+Implicit Types Q : val heap_lang → iProp heap_lang Σ.
 
 (** Bind. *)
 Lemma wp_bind {E e} K Q :
-  wp (Σ:=Σ) E e (λ v, wp (Σ:=Σ) E (fill K (v2e v)) Q) ⊑ wp (Σ:=Σ) E (fill K e) Q.
-Proof.
-  by apply (wp_bind (Σ:=Σ) (K := fill K)), fill_is_ctx.
-Qed.
+  wp E e (λ v, wp E (fill K (v2e v)) Q) ⊑ wp E (fill K e) Q.
+Proof. apply (wp_bind (K:=fill K)), fill_is_ctx. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 
@@ -17,9 +18,9 @@ Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 :
   E1 ⊆ E2 → to_val e1 = None →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → ef = None ∧ φ e2 σ2) →
-  pvs E2 E1 (ownP (Σ:=Σ) σ1 ★ ▷ ∀ e2 σ2, (■ φ e2 σ2 ∧ ownP (Σ:=Σ) σ2) -★
-    pvs E1 E2 (wp (Σ:=Σ) E2 e2 Q))
-  ⊑ wp (Σ:=Σ) E2 e1 Q.
+  pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2, (■ φ e2 σ2 ∧ ownP σ2) -★
+    pvs E1 E2 (wp E2 e2 Q))
+  ⊑ wp E2 e1 Q.
 Proof.
   intros ? He Hsafe Hstep.
   (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
@@ -45,8 +46,8 @@ Qed.
    postcondition a predicate over a *location* *)
 Lemma wp_alloc_pst E σ e v Q :
   e2v e = Some v →
-  (ownP (Σ:=Σ) σ ★ ▷(∀ l, ■(σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ) -★ Q (LocV l)))
-       ⊑ wp (Σ:=Σ) E (Alloc e) Q.
+  (ownP σ ★ ▷(∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
+       ⊑ wp E (Alloc e) Q.
 Proof.
   (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *)
   intros Hvl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
@@ -72,7 +73,7 @@ Qed.
 
 Lemma wp_load_pst E σ l v Q :
   σ !! l = Some v →
-  (ownP (Σ:=Σ) σ ★ ▷(ownP σ -★ Q v)) ⊑ wp (Σ:=Σ) E (Load (Loc l)) Q.
+  (ownP σ ★ ▷(ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
 Proof.
   intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
     (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first.
@@ -93,7 +94,7 @@ Qed.
 Lemma wp_store_pst E σ l e v v' Q :
   e2v e = Some v →
   σ !! l = Some v' →
-  (ownP (Σ:=Σ) σ ★ ▷(ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp (Σ:=Σ) E (Store (Loc l) e) Q.
+  (ownP σ ★ ▷(ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp E (Store (Loc l) e) Q.
 Proof.
   intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
     (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first.
@@ -114,17 +115,12 @@ Qed.
 Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
   e2v e1 = Some v1 → e2v e2 = Some v2 →
   σ !! l = Some v' → v' <> v1 →
-  (ownP (Σ:=Σ) σ ★ ▷(ownP σ -★ Q LitFalseV)) ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q.
+  (ownP σ ★ ▷(ownP σ -★ Q LitFalseV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
   intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', e' = LitFalse ∧ σ' = σ); last first.
-  - intros e2' σ2' ef Hstep. inversion_clear Hstep; first done.
-    (* FIXME this rewriting is rather ugly. *)
-    exfalso. rewrite Hvl in Hv1. case:Hv1=>?; subst v1. rewrite Hlookup in H.
-    case:H=>?; subst v'. done.
-  - do 3 eexists. eapply CasFailS; eassumption.
-  - reflexivity.
-  - reflexivity.
+    (φ := λ e' σ', e' = LitFalse ∧ σ' = σ) (E1:=E); auto; last first.
+  - by inversion_clear 1; simplify_map_equality.
+  - do 3 eexists; econstructor; eauto.
   - rewrite -pvs_intro.
     apply sep_mono; first done. apply later_mono.
     apply forall_intro=>e2'. apply forall_intro=>σ2'.
@@ -137,7 +133,7 @@ Qed.
 Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
   e2v e1 = Some v1 → e2v e2 = Some v2 →
   σ !! l = Some v1 →
-  (ownP (Σ:=Σ) σ ★ ▷(ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q.
+  (ownP σ ★ ▷(ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
   intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
     (φ := λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ); last first.
@@ -162,7 +158,8 @@ Qed.
 (** Base axioms for core primitives of the language: Stateless reductions *)
 
 Lemma wp_fork E e :
-  ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp (Σ:=Σ) E (Fork e) (λ v, ■(v = LitUnitV)).
+  ▷ wp coPset_all e (λ _, True : iProp heap_lang Σ)
+  ⊑ wp E (Fork e) (λ v, ■(v = LitUnitV)).
 Proof.
   etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e' ef, e' = LitUnit ∧ ef = Some e);
@@ -175,21 +172,16 @@ Proof.
     eapply ForkS.
   - reflexivity.
   - apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>ef.
-    apply impl_intro_l. apply const_elim_l. intros [-> ->].
-    (* FIXME RJ This is ridicolous. *)
-    transitivity (True ★ wp coPset_all e (λ _ : ival Σ, True))%I;
-      first by rewrite left_id.
-    apply sep_mono; last reflexivity.
-    rewrite -wp_value'; last reflexivity.
-    by apply const_intro.
+    apply forall_intro=>e2; apply forall_intro=>ef.
+    apply impl_intro_l, const_elim_l=>-[-> ->] /=; apply sep_intro_True_l; auto.
+    by rewrite -wp_value' //; apply const_intro.
 Qed.
 
 Lemma wp_lift_pure_step E (φ : expr → Prop) Q e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ ef = None ∧ φ e2) →
-  (▷ ∀ e2, ■ φ e2 → wp (Σ:=Σ) E e2 Q) ⊑ wp (Σ:=Σ) E e1 Q.
+  (▷ ∀ e2, ■ φ e2 → wp E e2 Q) ⊑ wp E e1 Q.
 Proof.
   intros He Hsafe Hstep.
   (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
@@ -209,7 +201,7 @@ Qed.
 
 Lemma wp_rec E ef e v Q :
   e2v e = Some v →
-  ▷wp (Σ:=Σ) E ef.[Rec ef, e /] Q ⊑ wp (Σ:=Σ) E (App (Rec ef) e) Q.
+  ▷wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
 Proof.
   etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = ef.[Rec ef, e /]); last first.
@@ -221,7 +213,7 @@ Proof.
 Qed.
 
 Lemma wp_plus n1 n2 E Q :
-  ▷Q (LitNatV (n1 + n2)) ⊑ wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
+  ▷Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
 Proof.
   etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = LitNat (n1 + n2)); last first.
@@ -235,7 +227,7 @@ Qed.
 
 Lemma wp_le_true n1 n2 E Q :
   n1 ≤ n2 →
-  ▷Q LitTrueV ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
+  ▷Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros Hle. etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = LitTrue); last first.
@@ -250,7 +242,7 @@ Qed.
 
 Lemma wp_le_false n1 n2 E Q :
   n1 > n2 →
-  ▷Q LitFalseV ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
+  ▷Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros Hle. etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = LitFalse); last first.
@@ -265,7 +257,7 @@ Qed.
 
 Lemma wp_fst e1 v1 e2 v2 E Q :
   e2v e1 = Some v1 → e2v e2 = Some v2 →
-  ▷Q v1 ⊑ wp (Σ:=Σ) E (Fst (Pair e1 e2)) Q.
+  ▷Q v1 ⊑ wp E (Fst (Pair e1 e2)) Q.
 Proof.
   intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = e1); last first.
@@ -279,7 +271,7 @@ Qed.
 
 Lemma wp_snd e1 v1 e2 v2 E Q :
   e2v e1 = Some v1 → e2v e2 = Some v2 →
-  ▷Q v2 ⊑ wp (Σ:=Σ) E (Snd (Pair e1 e2)) Q.
+  ▷Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
 Proof.
   intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = e2); last first.
@@ -293,7 +285,7 @@ Qed.
 
 Lemma wp_case_inl e0 v0 e1 e2 E Q :
   e2v e0 = Some v0 →
-  ▷wp (Σ:=Σ) E e1.[e0/] Q ⊑ wp (Σ:=Σ) E (Case (InjL e0) e1 e2) Q.
+  ▷wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q.
 Proof.
   intros Hv0. etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = e1.[e0/]); last first.
@@ -306,7 +298,7 @@ Qed.
 
 Lemma wp_case_inr e0 v0 e1 e2 E Q :
   e2v e0 = Some v0 →
-  ▷wp (Σ:=Σ) E e2.[e0/] Q ⊑ wp (Σ:=Σ) E (Case (InjR e0) e1 e2) Q.
+  ▷wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q.
 Proof.
   intros Hv0. etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = e2.[e0/]); last first.
@@ -322,7 +314,7 @@ Qed.
 Lemma wp_le n1 n2 E P Q :
   (n1 ≤ n2 → P ⊑ ▷Q LitTrueV) →
   (n1 > n2 → P ⊑ ▷Q LitFalseV) →
-  P ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
+  P ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros HPle HPgt.
   assert (Decision (n1 ≤ n2)) as Hn12 by apply _.
@@ -330,3 +322,4 @@ Proof.
   - rewrite -wp_le_true; auto.
   - assert (n1 > n2) by omega. rewrite -wp_le_false; auto.
 Qed.
+End lifting.
diff --git a/barrier/parameter.v b/barrier/parameter.v
deleted file mode 100644
index c3d21e55241b3108804e13ade1ef59a5bc1d7e1e..0000000000000000000000000000000000000000
--- a/barrier/parameter.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Export barrier.heap_lang.
-Require Import iris.parameter.
-
-Definition Σ := IParamConst heap_lang unitRA.
diff --git a/barrier/sugar.v b/barrier/sugar.v
index 559bd51f97382b41ff8a8ecf7543b517ba80ee55..d8fe3920f7050bc84ec8273341b3846ef15dc517 100644
--- a/barrier/sugar.v
+++ b/barrier/sugar.v
@@ -16,10 +16,14 @@ Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
 Definition LetCtx (K1 : ectx) (e2 : {bind expr}) := AppRCtx (LamV e2) K1.
 Definition SeqCtx (K1 : ectx) (e2 : expr) := LetCtx K1 (e2.[ren(+1)]).
 
+Section suger.
+Context {Σ : iFunctor}.
+Implicit Types P : iProp heap_lang Σ.
+Implicit Types Q : val heap_lang → iProp heap_lang Σ.
+
 (** Proof rules for the sugar *)
 Lemma wp_lam E ef e v Q :
-  e2v e = Some v →
-  ▷wp (Σ:=Σ) E ef.[e/] Q ⊑ wp (Σ:=Σ) E (App (Lam ef) e) Q.
+  e2v e = Some v → ▷wp E ef.[e/] Q ⊑ wp E (App (Lam ef) e) Q.
 Proof.
   intros Hv. rewrite -wp_rec; last eassumption.
   (* RJ: This pulls in functional extensionality. If that bothers us, we have
@@ -28,20 +32,20 @@ Proof.
 Qed.
 
 Lemma wp_let e1 e2 E Q :
-  wp (Σ:=Σ) E e1 (λ v, ▷wp (Σ:=Σ) E (e2.[v2e v/]) Q) ⊑ wp (Σ:=Σ) E (Let e1 e2) Q.
+  wp E e1 (λ v, ▷wp E (e2.[v2e v/]) Q) ⊑ wp E (Let e1 e2) Q.
 Proof.
   rewrite -(wp_bind (LetCtx EmptyCtx e2)). apply wp_mono=>v.
   rewrite -wp_lam //. by rewrite v2v.
 Qed.
 
 Lemma wp_if_true e1 e2 E Q :
-  ▷wp (Σ:=Σ) E e1 Q ⊑ wp (Σ:=Σ) E (If LitTrue e1 e2) Q.
+  ▷wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q.
 Proof.
   rewrite -wp_case_inl //. by asimpl.
 Qed.
 
 Lemma wp_if_false e1 e2 E Q :
-  ▷wp (Σ:=Σ) E e2 Q ⊑ wp (Σ:=Σ) E (If LitFalse e1 e2) Q.
+  ▷wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q.
 Proof.
   rewrite -wp_case_inr //. by asimpl.
 Qed.
@@ -49,7 +53,7 @@ Qed.
 Lemma wp_lt n1 n2 E P Q :
   (n1 < n2 → P ⊑ ▷Q LitTrueV) →
   (n1 ≥ n2 → P ⊑ ▷Q LitFalseV) →
-  P ⊑ wp (Σ:=Σ) E (Lt (LitNat n1) (LitNat n2)) Q.
+  P ⊑ wp E (Lt (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros HPlt HPge.
   rewrite -(wp_bind (LeLCtx EmptyCtx _)) -wp_plus -later_intro. simpl.
@@ -59,7 +63,7 @@ Qed.
 Lemma wp_eq n1 n2 E P Q :
   (n1 = n2 → P ⊑ ▷Q LitTrueV) →
   (n1 ≠ n2 → P ⊑ ▷Q LitFalseV) →
-  P ⊑ wp (Σ:=Σ) E (Eq (LitNat n1) (LitNat n2)) Q.
+  P ⊑ wp E (Eq (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros HPeq HPne.
   rewrite -wp_let -wp_value' // -later_intro. asimpl.
@@ -72,3 +76,4 @@ Proof.
   - asimpl. rewrite -wp_case_inr // -later_intro -wp_value' //.
     apply HPne; omega.
 Qed.
+End suger.
diff --git a/barrier/tests.v b/barrier/tests.v
index eb3ce36c13243f6543acad85c2859cd55964522f..fa6c63b041f4f735a009911d28eec901dfdc4838 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -25,16 +25,16 @@ Module LangTests.
   Qed.
 End LangTests.
 
-Module ParamTests.
-  Print Assumptions Σ.
-End ParamTests.
-
 Module LiftingTests.
+  Context {Σ : iFunctor}.
+  Implicit Types P : iProp heap_lang Σ.
+  Implicit Types Q : val heap_lang → iProp heap_lang Σ.
+
   (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
   Definition e3 := Load (Var 0).
   Definition e2 := Seq (Store (Var 0) (Plus (Load $ Var 0) (LitNat 1))) e3.
   Definition e := Let (Alloc (LitNat 1)) e2.
-  Goal ∀ σ E, (ownP (Σ:=Σ) σ) ⊑ (wp (Σ:=Σ) E e (λ v, ■(v = LitNatV 2))).
+  Goal ∀ σ E, (ownP σ : iProp heap_lang Σ) ⊑ (wp E e (λ v, ■(v = LitNatV 2))).
   Proof.
     move=> σ E. rewrite /e.
     rewrite -wp_let. rewrite -wp_alloc_pst; last done.
@@ -74,7 +74,7 @@ Module LiftingTests.
 
   Lemma FindPred_spec n1 n2 E Q :
     (■(n1 < n2) ∧ Q (LitNatV $ pred n2)) ⊑
-       wp (Σ:=Σ) E (App (FindPred (LitNat n2)) (LitNat n1)) Q.
+       wp E (App (FindPred (LitNat n2)) (LitNat n1)) Q.
   Proof.
     revert n1. apply löb_all_1=>n1.
     rewrite -wp_rec //. asimpl.
@@ -104,7 +104,7 @@ Module LiftingTests.
   Qed.
 
   Lemma Pred_spec n E Q :
-    ▷Q (LitNatV $ pred n) ⊑ wp (Σ:=Σ) E (App Pred (LitNat n)) Q.
+    ▷Q (LitNatV $ pred n) ⊑ wp E (App Pred (LitNat n)) Q.
   Proof.
     rewrite -wp_lam //. asimpl.
     rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
@@ -118,7 +118,9 @@ Module LiftingTests.
       + done.
   Qed.
 
-  Goal ∀ E, True ⊑ wp (Σ:=Σ) E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
+  Goal ∀ E,
+    (True : iProp heap_lang Σ)
+    ⊑ wp E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
   Proof.
     intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
     asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)
diff --git a/iris/adequacy.v b/iris/adequacy.v
index fed684c55fbd145eb1fb5828409bf9ce6f2a17a3..27d5ab13d304efdc35007edf55c3c541563845fd 100644
--- a/iris/adequacy.v
+++ b/iris/adequacy.v
@@ -7,9 +7,10 @@ Local Hint Extern 10 (✓{_} _) =>
   solve_validN.
 
 Section adequacy.
-Context {Σ : iParam}.
-Implicit Types e : iexpr Σ.
-Implicit Types Q : ival Σ → iProp Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types e : expr Λ.
+Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 Transparent uPred_holds.
 
 Notation wptp n := (Forall3 (λ e Q r, uPred_holds (wp coPset_all e Q) n r)).
@@ -46,7 +47,7 @@ Proof.
   * apply (IH (Qs1 ++ Q :: Qs2) (rs1 ++ r2 â‹… r2' :: rs2)).
     { rewrite /option_list right_id_L.
       apply Forall3_app, Forall3_cons; eauto using wptp_le.
-      apply uPred_weaken with r2 (k + n); eauto using @ra_included_l. }
+      apply uPred_weaken with r2 (k + n); eauto using cmra_included_l. }
     by rewrite -Permutation_middle /= big_op_app.
 Qed.
 Lemma ht_adequacy_steps P Q k n e1 t2 σ1 σ2 r1 :
@@ -60,7 +61,7 @@ Proof.
   intros Hht ????; apply (nsteps_wptp [pvs coPset_all coPset_all ∘ Q] k n
     ([e1],σ1) (t2,σ2) [r1]); rewrite /big_op ?right_id; auto.
   constructor; last constructor.
-  apply Hht with r1 (k + n); eauto using @ra_included_unit.
+  apply Hht with r1 (k + n); eauto using cmra_included_unit.
   by destruct (k + n).
 Qed.
 Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
@@ -70,15 +71,16 @@ Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
   ∃ rs2 Qs', wptp 3 t2 ((λ v, pvs coPset_all coPset_all (Q v)) :: Qs') rs2 ∧
              wsat 3 coPset_all σ2 (big_op rs2).
 Proof.
-  intros Hv ? [k ?]%rtc_nsteps. eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) m)); eauto; [|].
-  - by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN.
-  - exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ m). split_ands.
-    + by rewrite /op /cmra_op /= /res_op /= !ra_empty_l ra_empty_r.
-    + by rewrite /uPred_holds /=.
-    + by apply ownG_spec.
+  intros Hv ? [k ?]%rtc_nsteps.
+  eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) m)); eauto; [|].
+  { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
+  exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ m); split_ands.
+  * by rewrite Res_op ?left_id ?right_id.
+  * by rewrite /uPred_holds /=.
+  * by apply ownG_spec.
 Qed.
 Theorem ht_adequacy_result E φ e v t2 σ1 m σ2 :
-  ✓m →
+  ✓ m →
   {{ ownP σ1 ★ ownG m }} e @ E {{ λ v', ■ φ v' }} →
   rtc step ([e], σ1) (of_val v :: t2, σ2) →
   φ v.
@@ -92,7 +94,7 @@ Proof.
   by rewrite right_id_L.
 Qed.
 Lemma ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2 :
-  ✓m →
+  ✓ m →
   {{ ownP σ1 ★ ownG m }} e1 @ E {{ Q }} →
   rtc step ([e1], σ1) (t2, σ2) →
   e2 ∈ t2 → to_val e2 = None → reducible e2 σ2.
@@ -106,7 +108,7 @@ Proof.
     rewrite ?right_id_L ?big_op_delete; auto.
 Qed.
 Theorem ht_adequacy_safe E Q e1 t2 σ1 m σ2 :
-  ✓m →
+  ✓ m →
   {{ ownP σ1 ★ ownG m }} e1 @ E {{ Q }} →
   rtc step ([e1], σ1) (t2, σ2) →
   Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
diff --git a/iris/functor.v b/iris/functor.v
new file mode 100644
index 0000000000000000000000000000000000000000..49c7a0dfe2b3ad1a6ba3557ed0150b55fea9d388
--- /dev/null
+++ b/iris/functor.v
@@ -0,0 +1,26 @@
+Require Export modures.cmra.
+
+Structure iFunctor := IFunctor {
+  ifunctor_car :> cofeT → cmraT;
+  ifunctor_empty A : Empty (ifunctor_car A);
+  ifunctor_identity A : CMRAIdentity (ifunctor_car A);
+  ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
+  ifunctor_map_ne {A B} n : Proper (dist n ==> dist n) (@ifunctor_map A B);
+  ifunctor_map_id {A : cofeT} (x : ifunctor_car A) : ifunctor_map cid x ≡ x;
+  ifunctor_map_compose {A B C} (f : A -n> B) (g : B -n> C) x :
+    ifunctor_map (g ◎ f) x ≡ ifunctor_map g (ifunctor_map f x);
+  ifunctor_map_mono {A B} (f : A -n> B) : CMRAMonotone (ifunctor_map f)
+}.
+Existing Instances ifunctor_empty ifunctor_identity.
+Existing Instances ifunctor_map_ne ifunctor_map_mono.
+
+Lemma ifunctor_map_ext (Σ : iFunctor) {A B} (f g : A -n> B) m :
+  (∀ x, f x ≡ g x) → ifunctor_map Σ f m ≡ ifunctor_map Σ g m.
+Proof.
+  by intros; apply equiv_dist=> n; apply ifunctor_map_ne=> ?; apply equiv_dist.
+Qed.
+
+Program Definition iFunctor_const (icmra : cmraT) {icmra_empty : Empty icmra}
+    {icmra_identity : CMRAIdentity icmra} : iFunctor :=
+  {| ifunctor_car A := icmra; ifunctor_map A B f := cid |}.
+Solve Obligations with done.
\ No newline at end of file
diff --git a/iris/hoare.v b/iris/hoare.v
index 1f3885b4eb1971476fa7120cbd32ffc1e217ecf1..edfc9e54f9e8068f2fe32a20be73aea776db7cef 100644
--- a/iris/hoare.v
+++ b/iris/hoare.v
@@ -1,9 +1,9 @@
 Require Export iris.weakestpre iris.viewshifts.
 
-Definition ht {Σ} (E : coPset) (P : iProp Σ)
-    (e : iexpr Σ) (Q : ival Σ → iProp Σ) : iProp Σ :=
+Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
+    (e : expr Λ) (Q : val Λ → iProp Λ Σ) : iProp Λ Σ :=
   (□ (P → wp E e (λ v, pvs E E (Q v))))%I.
-Instance: Params (@ht) 2.
+Instance: Params (@ht) 3.
 
 Notation "{{ P } } e @ E {{ Q } }" := (ht E P e Q)
   (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : uPred_scope.
@@ -11,27 +11,27 @@ Notation "{{ P } } e @ E {{ Q } }" := (True ⊑ ht E P e Q)
   (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : C_scope.
 
 Section hoare.
-Context {Σ : iParam}.
-Implicit Types P : iProp Σ.
-Implicit Types Q : ival Σ → iProp Σ.
-Implicit Types v : ival Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P : iProp Λ Σ.
+Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types v : val Λ.
 Import uPred.
 
 Global Instance ht_ne E n :
-  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (@ht Σ E).
+  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
 Global Instance ht_proper E :
-  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Σ E).
+  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
 Lemma ht_mono E P P' Q Q' e :
   P ⊑ P' → (∀ v, Q' v ⊑ Q v) → {{ P' }} e @ E {{ Q' }} ⊑ {{ P }} e @ E {{ Q }}.
 Proof. by intros HP HQ; rewrite /ht -HP; setoid_rewrite HQ. Qed.
 Global Instance ht_mono' E :
-  Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Σ E).
+  Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed.
 
 Lemma ht_val E v :
-  {{ True }} of_val v @ E {{ λ v', ■ (v = v') }}.
+  {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', ■ (v = v') }}.
 Proof.
   apply (always_intro' _ _), impl_intro_l.
   by rewrite -wp_value -pvs_intro; apply const_intro.
diff --git a/iris/hoare_lifting.v b/iris/hoare_lifting.v
index df791cf698fcadf6006316c7308155bdb2f08962..5e5467f1bf64845cbabbc80207557367d4f3c045 100644
--- a/iris/hoare_lifting.v
+++ b/iris/hoare_lifting.v
@@ -8,12 +8,14 @@ Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
   (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : C_scope.
 
 Section lifting.
-Context {Σ : iParam}.
-Implicit Types e : iexpr Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types e : expr Λ.
+Implicit Types P : iProp Λ Σ.
+Implicit Types R : val Λ → iProp Λ Σ.
 Import uPred.
 
 Lemma ht_lift_step E1 E2
-    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P P' Q1 Q2 R e1 σ1 :
+    (φ : expr Λ → state Λ → option (expr Λ) → Prop) P P' Q1 Q2 R e1 σ1 :
   E1 ⊆ E2 → to_val e1 = None →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
@@ -42,8 +44,7 @@ Proof.
   rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
   by apply const_intro.
 Qed.
-Lemma ht_lift_atomic E
-    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P e1 σ1 :
+Lemma ht_lift_atomic E (φ : expr Λ → state Λ → option (expr Λ) → Prop) P e1 σ1 :
   atomic e1 →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
@@ -68,7 +69,7 @@ Proof.
     rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
     by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro.
 Qed.
-Lemma ht_lift_pure_step E (φ : iexpr Σ → option (iexpr Σ) → Prop) P P' Q e1 :
+Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
@@ -94,7 +95,7 @@ Proof.
   by apply const_intro.
 Qed.
 Lemma ht_lift_pure_determistic_step E
-    (φ : iexpr Σ → option (iexpr Σ) → Prop) P P' Q e1 e2 ef :
+    (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 e2 ef :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
diff --git a/iris/language.v b/iris/language.v
index b3aa860f254bf8a0c7183223058e5d463688657b..9bb0fca56ebfd3a6092dd85cd768831d782e10ac 100644
--- a/iris/language.v
+++ b/iris/language.v
@@ -1,10 +1,13 @@
-Require Export modures.base.
+Require Export modures.cmra.
 
-Class Language (E V St : Type) := {
-  of_val : V → E;
-  to_val : E → option V;
-  atomic : E → Prop;
-  prim_step : E → St → E → St → option E → Prop;
+Structure language := Language {
+  expr : Type;
+  val : Type;
+  state : Type;
+  of_val : val → expr;
+  to_val : expr → option val;
+  atomic : expr → Prop;
+  prim_step : expr → state → expr → state → option expr → Prop;
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
   values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None;
@@ -14,31 +17,43 @@ Class Language (E V St : Type) := {
     prim_step e1 σ1 e2 σ2 ef →
     is_Some (to_val e2)
 }.
+Arguments of_val {_} _.
+Arguments to_val {_} _.
+Arguments atomic {_} _.
+Arguments prim_step {_} _ _ _ _ _.
+Arguments to_of_val {_} _.
+Arguments of_to_val {_} _ _ _.
+Arguments values_stuck {_} _ _ _ _ _ _.
+Arguments atomic_not_value {_} _ _.
+Arguments atomic_step {_} _ _ _ _ _ _ _.
+
+Canonical Structure istateC Σ := leibnizC (state Σ).
+
+Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
 
 Section language.
-  Context `{Language E V St}.
+  Context {Λ : language}.
+  Implicit Types v : val Λ.
 
-  Definition reducible (e : E) (σ : St) :=
+  Definition reducible (e : expr Λ) (σ : state Λ) :=
     ∃ e' σ' ef, prim_step e σ e' σ' ef.
+  Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
+    | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
+       ρ1 = (t1 ++ e1 :: t2, σ1) →
+       ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
+       prim_step e1 σ1 e2 σ2 ef →
+       step ρ1 ρ2.
+
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
-
   Lemma atomic_of_val v : ¬atomic (of_val v).
   Proof.
     by intros Hat; apply atomic_not_value in Hat; rewrite to_of_val in Hat.
   Qed.
-  Global Instance: Injective (=) (=) of_val.
+  Global Instance: Injective (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
 
-  Definition cfg : Type := (list E * St)%type.
-  Inductive step (ρ1 ρ2 : cfg) : Prop :=
-    | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
-       ρ1 = (t1 ++ e1 :: t2, σ1) →
-       ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
-       prim_step e1 σ1 e2 σ2 ef →
-       step ρ1 ρ2.
-
-  Record is_ctx (K : E → E) := IsCtx {
+  Record is_ctx (K : expr Λ → expr Λ) := IsCtx {
     is_ctx_value e : to_val e = None → to_val (K e) = None;
     is_ctx_step_preserved e1 σ1 e2 σ2 ef :
       prim_step e1 σ1 e2 σ2 ef → prim_step (K e1) σ1 (K e2) σ2 ef;
diff --git a/iris/lifting.v b/iris/lifting.v
index c94eda289e988da9ac0c8ea2dd2298a147a9437d..6e8c632bb5601dd2221f5ba79f17d6c84a9be2d7 100644
--- a/iris/lifting.v
+++ b/iris/lifting.v
@@ -7,14 +7,15 @@ Local Hint Extern 10 (✓{_} _) =>
   solve_validN.
 
 Section lifting.
-Context {Σ : iParam}.
-Implicit Types v : ival Σ.
-Implicit Types e : iexpr Σ.
-Implicit Types σ : istate Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+Implicit Types σ : state Λ.
+Implicit Types Q : val Λ → iProp Λ Σ.
 Transparent uPred_holds.
 
 Lemma wp_lift_step E1 E2
-    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) Q e1 σ1 :
+    (φ : expr Λ → state Λ → option (expr Λ) → Prop) Q e1 σ1 :
   E1 ⊆ E2 → to_val e1 = None →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
@@ -35,7 +36,7 @@ Proof.
   { rewrite (commutative _ r2) -(associative _); eauto using wsat_le. }
   by exists r1', r2'; split_ands; [| |by intros ? ->].
 Qed.
-Lemma wp_lift_pure_step E (φ : iexpr Σ → option (iexpr Σ) → Prop) Q e1 :
+Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Q e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
diff --git a/iris/model.v b/iris/model.v
index f6d146a2b03325f97ad927af83e67d331169c1b5..6fde393bbf486b06a72d169c73c9378c281371d4 100644
--- a/iris/model.v
+++ b/iris/model.v
@@ -2,15 +2,17 @@ Require Export modures.logic iris.resources.
 Require Import modures.cofe_solver.
 
 Module iProp.
-Definition F (Σ : iParam) (A B : cofeT) : cofeT := uPredC (resRA Σ (laterC A)).
-Definition map {Σ : iParam} {A1 A2 B1 B2 : cofeT}
-    (f : (A2 -n> A1) * (B1 -n> B2)) : F Σ A1 B1 -n> F Σ A2 B2 :=
+Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
+  uPredC (resRA Λ Σ (laterC A)).
+Definition map {Λ : language} {Σ : iFunctor} {A1 A2 B1 B2 : cofeT}
+    (f : (A2 -n> A1) * (B1 -n> B2)) : F Λ Σ A1 B1 -n> F Λ Σ A2 B2 :=
   uPredC_map (resRA_map (laterC_map (f.1))).
-Definition result Σ : solution (F Σ).
+Definition result Λ Σ : solution (F Λ Σ).
 Proof.
-  apply (solver.result _ (@map Σ)).
-  * intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=>r {P} /=.
-    rewrite -{2}(res_map_id r). apply res_map_ext=>{r} r /=. by rewrite later_map_id.
+  apply (solver.result _ (@map Λ Σ)).
+  * intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=> r.
+    rewrite /= -{2}(res_map_id r); apply res_map_ext=>{r} r /=.
+    by rewrite later_map_id.
   * intros A1 A2 A3 B1 B2 B3 f g f' g' P. rewrite /map /=.
     rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
     rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
@@ -21,22 +23,24 @@ Qed.
 End iProp.
 
 (* Solution *)
-Definition iPreProp (Σ : iParam) : cofeT := iProp.result Σ.
-Notation iRes Σ := (res Σ (laterC (iPreProp Σ))).
-Notation iResRA Σ := (resRA Σ (laterC (iPreProp Σ))).
-Notation iWld Σ := (mapRA positive (agreeRA (laterC (iPreProp Σ)))).
-Notation iPst Σ := (exclRA (istateC Σ)).
-Notation iGst Σ := (icmra Σ (laterC (iPreProp Σ))).
-Definition iProp (Σ : iParam) : cofeT := uPredC (iResRA Σ).
-Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := solution_fold _.
-Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
-Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
+Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp.result Λ Σ.
+Notation iRes Λ Σ := (res Λ Σ (laterC (iPreProp Λ Σ))).
+Notation iResRA Λ Σ := (resRA Λ Σ (laterC (iPreProp Λ Σ))).
+Notation iWld Λ Σ := (mapRA positive (agreeRA (laterC (iPreProp Λ Σ)))).
+Notation iPst Λ := (exclRA (istateC Λ)).
+Notation iGst Λ Σ := (ifunctor_car Σ (laterC (iPreProp Λ Σ))).
+Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResRA Λ Σ).
+Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ := solution_fold _.
+Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.
+Lemma iProp_fold_unfold {Λ Σ} (P : iProp Λ Σ) : iProp_fold (iProp_unfold P) ≡ P.
 Proof. apply solution_unfold_fold. Qed.
-Lemma iProp_unfold_fold {Σ} (P : iPreProp Σ) : iProp_unfold (iProp_fold P) ≡ P.
+Lemma iProp_unfold_fold {Λ Σ} (P : iPreProp Λ Σ) :
+  iProp_unfold (iProp_fold P) ≡ P.
 Proof. apply solution_fold_unfold. Qed.
 Bind Scope uPred_scope with iProp.
 
-Instance iProp_fold_inj n Σ : Injective (dist n) (dist n) (@iProp_fold Σ).
+Instance iProp_fold_inj n Λ Σ : Injective (dist n) (dist n) (@iProp_fold Λ Σ).
 Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
-Instance iProp_unfold_inj n Σ : Injective (dist n) (dist n) (@iProp_unfold Σ).
+Instance iProp_unfold_inj n Λ Σ :
+  Injective (dist n) (dist n) (@iProp_unfold Λ Σ).
 Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.
diff --git a/iris/ownership.v b/iris/ownership.v
index 98bfc972182944ef77c83e3c3644049f84015983..fc168f419792c322719e1cefe6c7ff03827f102c 100644
--- a/iris/ownership.v
+++ b/iris/ownership.v
@@ -1,25 +1,25 @@
 Require Export iris.model.
 
-Definition inv {Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+Definition inv {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
   uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
-Arguments inv {_} _ _%I.
-Definition ownP {Σ} (σ : istate Σ) : iProp Σ := uPred_own (Res ∅ (Excl σ) ∅).
-Definition ownG {Σ} (m : iGst Σ) : iProp Σ := uPred_own (Res ∅ ∅ m).
-Instance: Params (@inv) 2.
-Instance: Params (@ownP) 1.
-Instance: Params (@ownG) 1.
+Arguments inv {_ _} _ _%I.
+Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_own (Res ∅ (Excl σ) ∅).
+Definition ownG {Λ Σ} (m : iGst Λ Σ) : iProp Λ Σ := uPred_own (Res ∅ ∅ m).
+Instance: Params (@inv) 3.
+Instance: Params (@ownP) 2.
+Instance: Params (@ownG) 2.
 
 Typeclasses Opaque inv ownG ownP.
 
 Section ownership.
-Context {Σ : iParam}.
-Implicit Types r : iRes Σ.
-Implicit Types σ : istate Σ.
-Implicit Types P : iProp Σ.
-Implicit Types m : iGst Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types r : iRes Λ Σ.
+Implicit Types σ : state Λ.
+Implicit Types P : iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 
 (* Invariants *)
-Global Instance inv_contractive i : Contractive (@inv Σ i).
+Global Instance inv_contractive i : Contractive (@inv Λ Σ i).
 Proof.
   intros n P Q HPQ.
   apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
@@ -27,7 +27,8 @@ Proof.
 Qed.
 Lemma always_inv i P : (□ inv i P)%I ≡ inv i P.
 Proof.
-  by apply uPred.always_own; rewrite Res_unit !ra_unit_empty map_unit_singleton.
+  apply uPred.always_own.
+  by rewrite Res_unit !cmra_unit_empty map_unit_singleton.
 Qed.
 Global Instance inv_always_stable i P : AlwaysStable (inv i P).
 Proof. by rewrite /AlwaysStable always_inv. Qed.
@@ -35,28 +36,29 @@ Lemma inv_sep_dup i P : inv i P ≡ (inv i P ★ inv i P)%I.
 Proof. apply (uPred.always_sep_dup' _). Qed.
 
 (* physical state *)
-Lemma ownP_twice σ1 σ2 : (ownP σ1 ★ ownP σ2 : iProp Σ) ⊑ False.
+Lemma ownP_twice σ1 σ2 : (ownP σ1 ★ ownP σ2 : iProp Λ Σ) ⊑ False.
 Proof.
   rewrite /ownP -uPred.own_op Res_op.
   by apply uPred.own_invalid; intros (_&?&_).
 Qed.
-Global Instance ownP_timeless σ : TimelessP (ownP σ).
+Global Instance ownP_timeless σ : TimelessP (@ownP Λ Σ σ).
 Proof. rewrite /ownP; apply _. Qed.
 
 (* ghost state *)
-Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Σ).
+Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
 Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
-Global Instance ownG_proper : Proper ((≡) ==> (≡)) (@ownG Σ) := ne_proper _.
+Global Instance ownG_proper : Proper ((≡) ==> (≡)) (@ownG Λ Σ) := ne_proper _.
 Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ≡ (ownG m1 ★ ownG m2)%I.
 Proof. by rewrite /ownG -uPred.own_op Res_op !(left_id _ _). Qed.
 Lemma always_ownG_unit m : (□ ownG (unit m))%I ≡ ownG (unit m).
 Proof.
-  by apply uPred.always_own; rewrite Res_unit !ra_unit_empty ra_unit_idempotent.
+  apply uPred.always_own.
+  by rewrite Res_unit !cmra_unit_empty cmra_unit_idempotent.
 Qed.
 Lemma ownG_valid m : (ownG m) ⊑ (✓ m).
 Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
 Lemma ownG_valid_r m : (ownG m) ⊑ (ownG m ★ ✓ m).
-Proof. apply uPred.always_entails_r', ownG_valid; by apply _. Qed.
+Proof. apply (uPred.always_entails_r' _ _), ownG_valid. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
 
@@ -69,15 +71,15 @@ Proof.
   * intros [(P'&Hi&HP) _]; rewrite Hi.
     by apply Some_dist, symmetry, agree_valid_includedN,
       (cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
-  * intros ?; split_ands; try apply cmra_empty_least; eauto.
+  * intros ?; split_ands; try apply cmra_empty_leastN; eauto.
 Qed.
 Lemma ownP_spec r n σ : ✓{n} r → (ownP σ) n r ↔ pst r ={n}= Excl σ.
 Proof.
   intros (?&?&?); rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
-  naive_solver (apply cmra_empty_least).
+  naive_solver (apply cmra_empty_leastN).
 Qed.
 Lemma ownG_spec r n m : (ownG m) n r ↔ m ≼{n} gst r.
 Proof.
-  rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_least).
+  rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_leastN).
 Qed.
 End ownership.
diff --git a/iris/parameter.v b/iris/parameter.v
deleted file mode 100644
index cfbf73ee39c65de9138adace5faa06ee88e87e32..0000000000000000000000000000000000000000
--- a/iris/parameter.v
+++ /dev/null
@@ -1,41 +0,0 @@
-Require Export modures.cmra iris.language.
-
-Record iParam := IParam {
-  iexpr : Type;
-  ival : Type;
-  istate : Type;
-  ilanguage : Language iexpr ival istate;
-  icmra : cofeT → cmraT;
-  icmra_empty A : Empty (icmra A);
-  icmra_empty_spec A : RAIdentity (icmra A);
-  icmra_empty_timeless A : Timeless (∅ : icmra A);
-  icmra_map {A B} (f : A -n> B) : icmra A -n> icmra B;
-  icmra_map_ne {A B} n : Proper (dist n ==> dist n) (@icmra_map A B);
-  icmra_map_id {A : cofeT} (x : icmra A) : icmra_map cid x ≡ x;
-  icmra_map_compose {A B C} (f : A -n> B) (g : B -n> C) x :
-    icmra_map (g ◎ f) x ≡ icmra_map g (icmra_map f x);
-  icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f)
-}.
-Arguments IParam {_ _ _} ilanguage icmra {_ _ _} _ {_ _ _ _}.
-Existing Instances ilanguage.
-Existing Instances icmra_empty icmra_empty_spec icmra_empty_timeless.
-Existing Instances icmra_map_ne icmra_map_mono.
-
-Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
-  (∀ x, f x ≡ g x) → icmra_map Σ f m ≡ icmra_map Σ g m.
-Proof.
-  by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
-Qed.
-
-Canonical Structure istateC Σ := leibnizC (istate Σ).
-
-Definition IParamConst {iexpr ival istate : Type}
-           (ilanguage : Language iexpr ival istate)
-           (icmra : cmraT) {icmra_empty : Empty icmra}
-           {icmra_empty_spec : RAIdentity icmra} {icmra_empty_timeless: Timeless (∅ : icmra)}:
-  iParam.
-eapply (IParam ilanguage (fun _ => icmra) (fun _ _ _ => cid)).
-Unshelve.
-- by intros.
-- by intros.
-Defined.
diff --git a/iris/pviewshifts.v b/iris/pviewshifts.v
index 81ee2f4eec368916dff1dd9f5a644d6597aa6a31..e84941e58d86e5bff8977822c14bacf9fd1249b7 100644
--- a/iris/pviewshifts.v
+++ b/iris/pviewshifts.v
@@ -7,38 +7,38 @@ Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
   solve_validN.
 
-Program Definition pvs {Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
   {| uPred_holds n r1 := ∀ rf k Ef σ,
        1 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ →
        wsat k (E1 ∪ Ef) σ (r1 ⋅ rf) →
        ∃ r2, P k r2 ∧ wsat k (E2 ∪ Ef) σ (r2 ⋅ rf) |}.
 Next Obligation.
-  intros Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
+  intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
   apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia.
 Qed.
-Next Obligation. intros Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed.
+Next Obligation. intros Λ Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed.
 Next Obligation.
-  intros Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
+  intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
   destruct (HP (r3⋅rf) k Ef σ) as (r'&?&Hws'); rewrite ?(associative op); auto.
   exists (r' â‹… r3); rewrite -(associative _); split; last done.
-  apply uPred_weaken with r' k; eauto using @ra_included_l.
+  apply uPred_weaken with r' k; eauto using cmra_included_l.
 Qed.
-Arguments pvs {_} _ _ _%I : simpl never.
-Instance: Params (@pvs) 3.
+Arguments pvs {_ _} _ _ _%I : simpl never.
+Instance: Params (@pvs) 4.
 
 Section pvs.
-Context {Σ : iParam}.
-Implicit Types P Q : iProp Σ.
-Implicit Types m : iGst Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P Q : iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 Transparent uPred_holds.
 
-Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
+Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
 Proof.
   intros P Q HPQ r1 n' ??; simpl; split; intros HP rf k Ef σ ???;
     destruct (HP rf k Ef σ) as (r2&?&?); auto;
     exists r2; split_ands; auto; apply HPQ; eauto.
 Qed.
-Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Σ E1 E2).
+Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2).
 Proof. apply ne_proper, _. Qed.
 
 Lemma pvs_intro E P : P ⊑ pvs E E P.
@@ -55,7 +55,7 @@ Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊑ pvs E E P.
 Proof.
   rewrite uPred.timelessP_spec=> HP r [|n] ? HP' rf k Ef σ ???; first lia.
   exists r; split; last done.
-  apply HP, uPred_weaken with r n; eauto using cmra_valid_le.
+  apply HP, uPred_weaken with r n; eauto using cmra_validN_le.
 Qed.
 Lemma pvs_trans E1 E2 E3 P :
   E2 ⊆ E1 ∪ E3 → pvs E1 E2 (pvs E2 E3 P) ⊑ pvs E1 E3 P.
@@ -85,7 +85,7 @@ Proof.
   destruct (wsat_open k Ef σ (r ⋅ rf) i P) as (rP&?&?); auto.
   { rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
   exists (rP â‹… r); split; last by rewrite (left_id_L _ _) -(associative _).
-  eapply uPred_weaken with rP (S k); eauto using @ra_included_l.
+  eapply uPred_weaken with rP (S k); eauto using cmra_included_l.
 Qed.
 Lemma pvs_close i P : (inv i P ∧ ▷ P) ⊑ pvs ∅ {[ i ]} True.
 Proof.
@@ -96,12 +96,12 @@ Proof.
   * by rewrite -(left_id_L ∅ (∪) Ef).
   * apply uPred_weaken with r n; auto.
 Qed.
-Lemma pvs_updateP E m (P : iGst Σ → Prop) :
+Lemma pvs_updateP E m (P : iGst Λ Σ → Prop) :
   m ⇝: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
 Proof.
   intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
   destruct (wsat_update_gst k (E ∪ Ef) σ r rf m P)
-    as (m'&?&?); eauto using cmra_included_le.
+    as (m'&?&?); eauto using cmra_includedN_le.
   by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
 Qed.
 Lemma pvs_alloc E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■ (i ∈ E) ∧ inv i P).
@@ -114,8 +114,9 @@ Proof.
 Qed.
 
 (* Derived rules *)
+Opaque uPred_holds.
 Import uPred.
-Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Σ E1 E2).
+Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
 Proof. intros P Q; apply pvs_mono. Qed.
 Lemma pvs_trans' E P : pvs E E (pvs E E P) ⊑ pvs E E P.
 Proof. apply pvs_trans; solve_elem_of. Qed.
diff --git a/iris/resources.v b/iris/resources.v
index 067b47e22eb219dccc9386f73c6d5fa2f3132875..d2692b7daf05efa57f3cc8c74d80f58a099fd789 100644
--- a/iris/resources.v
+++ b/iris/resources.v
@@ -1,56 +1,57 @@
-Require Export modures.fin_maps modures.agree modures.excl iris.parameter.
+Require Export modures.fin_maps modures.agree modures.excl.
+Require Export iris.language iris.functor.
 
-Record res (Σ : iParam) (A : cofeT) := Res {
+Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
   wld : mapRA positive (agreeRA A);
-  pst : exclRA (istateC Σ);
-  gst : icmra Σ A;
+  pst : exclRA (istateC Λ);
+  gst : Σ A;
 }.
 Add Printing Constructor res.
-Arguments Res {_ _} _ _ _.
-Arguments wld {_ _} _.
-Arguments pst {_ _} _.
-Arguments gst {_ _} _.
-Instance: Params (@Res) 2.
-Instance: Params (@wld) 2.
-Instance: Params (@pst) 2.
-Instance: Params (@gst) 2.
+Arguments Res {_ _ _} _ _ _.
+Arguments wld {_ _ _} _.
+Arguments pst {_ _ _} _.
+Arguments gst {_ _ _} _.
+Instance: Params (@Res) 3.
+Instance: Params (@wld) 3.
+Instance: Params (@pst) 3.
+Instance: Params (@gst) 3.
 
 Section res.
-Context {Σ : iParam} {A : cofeT}.
-Implicit Types r : res Σ A.
+Context {Λ : language} {Σ : iFunctor} {A : cofeT}.
+Implicit Types r : res Λ Σ A.
 
-Inductive res_equiv' (r1 r2 : res Σ A) := Res_equiv :
+Inductive res_equiv' (r1 r2 : res Λ Σ A) := Res_equiv :
   wld r1 ≡ wld r2 → pst r1 ≡ pst r2 → gst r1 ≡ gst r2 → res_equiv' r1 r2.
-Instance res_equiv : Equiv (res Σ A) := res_equiv'.
-Inductive res_dist' (n : nat) (r1 r2 : res Σ A) := Res_dist :
+Instance res_equiv : Equiv (res Λ Σ A) := res_equiv'.
+Inductive res_dist' (n : nat) (r1 r2 : res Λ Σ A) := Res_dist :
   wld r1 ={n}= wld r2 → pst r1 ={n}= pst r2 → gst r1 ={n}= gst r2 →
   res_dist' n r1 r2.
-Instance res_dist : Dist (res Σ A) := res_dist'.
+Instance res_dist : Dist (res Λ Σ A) := res_dist'.
 Global Instance Res_ne n :
-  Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Σ A).
+  Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Λ Σ A).
 Proof. done. Qed.
-Global Instance Res_proper : Proper ((≡) ==> (≡) ==> (≡) ==> (≡)) (@Res Σ A).
+Global Instance Res_proper : Proper ((≡) ==> (≡) ==> (≡) ==> (≡)) (@Res Λ Σ A).
 Proof. done. Qed.
-Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Σ A).
+Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Λ Σ A).
 Proof. by destruct 1. Qed.
-Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Σ A).
+Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Λ Σ A).
 Proof. by destruct 1. Qed.
-Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Σ A).
+Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ Σ A).
 Proof. by destruct 1. Qed.
-Global Instance pst_ne' n : Proper (dist (S n) ==> (≡)) (@pst Σ A).
+Global Instance pst_ne' n : Proper (dist (S n) ==> (≡)) (@pst Λ Σ A).
 Proof.
   intros σ σ' [???]; apply (timeless _), dist_le with (S n); auto with lia.
 Qed.
-Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Σ A).
+Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Λ Σ A).
 Proof. by destruct 1; unfold_leibniz. Qed.
-Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Σ A).
+Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ Σ A).
 Proof. by destruct 1. Qed.
-Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Σ A).
+Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Λ Σ A).
 Proof. by destruct 1. Qed.
-Instance res_compl : Compl (res Σ A) := λ c,
+Instance res_compl : Compl (res Λ Σ A) := λ c,
   Res (compl (chain_map wld c))
       (compl (chain_map pst c)) (compl (chain_map gst c)).
-Definition res_cofe_mixin : CofeMixin (res Σ A).
+Definition res_cofe_mixin : CofeMixin (res Λ Σ A).
 Proof.
   split.
   * intros w1 w2; split.
@@ -72,31 +73,30 @@ Global Instance res_timeless r :
   Timeless (wld r) → Timeless (gst r) → Timeless r.
 Proof. by destruct 3; constructor; try apply (timeless _). Qed.
 
-Instance res_op : Op (res Σ A) := λ r1 r2,
+Instance res_op : Op (res Λ Σ A) := λ r1 r2,
   Res (wld r1 â‹… wld r2) (pst r1 â‹… pst r2) (gst r1 â‹… gst r2).
-Global Instance res_empty : Empty (res Σ A) := Res ∅ ∅ ∅.
-Instance res_unit : Unit (res Σ A) := λ r,
+Global Instance res_empty : Empty (res Λ Σ A) := Res ∅ ∅ ∅.
+Instance res_unit : Unit (res Λ Σ A) := λ r,
   Res (unit (wld r)) (unit (pst r)) (unit (gst r)).
-Instance res_valid : Valid (res Σ A) := λ r, ✓ (wld r) ∧ ✓ (pst r) ∧ ✓ (gst r).
-Instance res_validN : ValidN (res Σ A) := λ n r,
+Instance res_validN : ValidN (res Λ Σ A) := λ n r,
   ✓{n} (wld r) ∧ ✓{n} (pst r) ∧ ✓{n} (gst r).
-Instance res_minus : Minus (res Σ A) := λ r1 r2,
+Instance res_minus : Minus (res Λ Σ A) := λ r1 r2,
   Res (wld r1 ⩪ wld r2) (pst r1 ⩪ pst r2) (gst r1 ⩪ gst r2).
-Lemma res_included (r1 r2 : res Σ A) :
+Lemma res_included (r1 r2 : res Λ Σ A) :
   r1 ≼ r2 ↔ wld r1 ≼ wld r2 ∧ pst r1 ≼ pst r2 ∧ gst r1 ≼ gst r2.
 Proof.
   split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
   intros [r Hr]; split_ands;
     [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
 Qed.
-Lemma res_includedN (r1 r2 : res Σ A) n :
+Lemma res_includedN (r1 r2 : res Λ Σ A) n :
   r1 ≼{n} r2 ↔ wld r1 ≼{n} wld r2 ∧ pst r1 ≼{n} pst r2 ∧ gst r1 ≼{n} gst r2.
 Proof.
   split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
   intros [r Hr]; split_ands;
     [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
 Qed.
-Definition res_cmra_mixin : CMRAMixin (res Σ A).
+Definition res_cmra_mixin : CMRAMixin (res Λ Σ A).
 Proof.
   split.
   * by intros n x [???] ? [???]; constructor; simpl in *; cofe_subst.
@@ -105,26 +105,19 @@ Proof.
   * by intros n [???] ? [???] [???] ? [???];
       constructor; simpl in *; cofe_subst.
   * done.
-  * by intros n ? (?&?&?); split_ands'; apply cmra_valid_S.
-  * intros r; unfold valid, res_valid, validN, res_validN.
-    rewrite !cmra_valid_validN; naive_solver.
+  * by intros n ? (?&?&?); split_ands'; apply cmra_validN_S.
   * intros ???; constructor; simpl; apply (associative _).
   * intros ??; constructor; simpl; apply (commutative _).
-  * intros ?; constructor; simpl; apply ra_unit_l.
-  * intros ?; constructor; simpl; apply ra_unit_idempotent.
+  * intros ?; constructor; simpl; apply cmra_unit_l.
+  * intros ?; constructor; simpl; apply cmra_unit_idempotent.
   * intros n r1 r2; rewrite !res_includedN.
-    by intros (?&?&?); split_ands'; apply cmra_unit_preserving.
+    by intros (?&?&?); split_ands'; apply cmra_unit_preservingN.
   * intros n r1 r2 (?&?&?);
-      split_ands'; simpl in *; eapply cmra_valid_op_l; eauto.
+      split_ands'; simpl in *; eapply cmra_validN_op_l; eauto.
   * intros n r1 r2; rewrite res_includedN; intros (?&?&?).
     by constructor; apply cmra_op_minus.
 Qed.
-Global Instance res_ra_empty : RAIdentity (res Σ A).
-Proof.
-  by repeat split; simpl; repeat apply ra_empty_valid; rewrite (left_id _ _).
-Qed.
-
-Definition res_cmra_extend_mixin : CMRAExtendMixin (res Σ A).
+Definition res_cmra_extend_mixin : CMRAExtendMixin (res Λ Σ A).
 Proof.
   intros n r r1 r2 (?&?&?) [???]; simpl in *.
   destruct (cmra_extend_op n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
@@ -134,14 +127,21 @@ Proof.
 Qed.
 Canonical Structure resRA : cmraT :=
   CMRAT res_cofe_mixin res_cmra_mixin res_cmra_extend_mixin.
+Global Instance res_cmra_identity : CMRAIdentity resRA.
+Proof.
+  split.
+  * intros n; split_ands'; apply cmra_empty_valid.
+  * by split; rewrite /= (left_id _ _).
+  * apply _.
+Qed.
 
-Definition update_pst (σ : istate Σ) (r : res Σ A) : res Σ A :=
+Definition update_pst (σ : state Λ) (r : res Λ Σ A) : res Λ Σ A :=
   Res (wld r) (Excl σ) (gst r).
-Definition update_gst (m : icmra Σ A) (r : res Σ A) : res Σ A :=
+Definition update_gst (m : Σ A) (r : res Λ Σ A) : res Λ Σ A :=
   Res (wld r) (pst r) m.
 
 Lemma wld_validN n r : ✓{n} r → ✓{n} (wld r).
-Proof. by intros (?&?&?). Qed. 
+Proof. by intros (?&?&?). Qed.
 Lemma gst_validN n r : ✓{n} r → ✓{n} (gst r).
 Proof. by intros (?&?&?). Qed.
 Lemma Res_op w1 w2 σ1 σ2 m1 m2 :
@@ -153,7 +153,7 @@ Lemma lookup_wld_op_l n r1 r2 i P :
   ✓{n} (r1⋅r2) → wld r1 !! i ={n}= Some P → (wld r1 ⋅ wld r2) !! i ={n}= Some P.
 Proof.
   move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
-  destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?(right_id _ _) // =>-> ?.
+  destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
   by constructor; rewrite (agree_op_inv P P') // agree_idempotent.
 Qed.
 Lemma lookup_wld_op_r n r1 r2 i P :
@@ -166,49 +166,50 @@ Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
 End res.
 Arguments resRA : clear implicits.
 
-Definition res_map {Σ A B} (f : A -n> B) (r : res Σ A) : res Σ B :=
+Definition res_map {Λ Σ A B} (f : A -n> B) (r : res Λ Σ A) : res Λ Σ B :=
   Res (agree_map f <$> (wld r))
       (pst r)
-      (icmra_map Σ f (gst r)).
-Instance res_map_ne Σ (A B : cofeT) (f : A -n> B) :
+      (ifunctor_map Σ f (gst r)).
+Instance res_map_ne Λ Σ (A B : cofeT) (f : A -n> B) :
   (∀ n, Proper (dist n ==> dist n) f) →
-  ∀ n, Proper (dist n ==> dist n) (@res_map Σ _ _ f).
+  ∀ n, Proper (dist n ==> dist n) (@res_map Λ Σ _ _ f).
 Proof. by intros Hf n [] ? [???]; constructor; simpl in *; cofe_subst. Qed.
-Lemma res_map_id {Σ A} (r : res Σ A) : res_map cid r ≡ r.
+Lemma res_map_id {Λ Σ A} (r : res Λ Σ A) : res_map cid r ≡ r.
 Proof.
   constructor; simpl; [|done|].
   * rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=.
     by rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=.
-  * by rewrite -{2}(icmra_map_id Σ (gst r)); apply icmra_map_ext=> m /=.
+  * by rewrite -{2}(ifunctor_map_id Σ (gst r)); apply ifunctor_map_ext=> m /=.
 Qed.
-Lemma res_map_compose {Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Σ A) :
+Lemma res_map_compose {Λ Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Λ Σ A) :
   res_map (g ◎ f) r ≡ res_map g (res_map f r).
 Proof.
   constructor; simpl; [|done|].
   * rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
     by rewrite -agree_map_compose; apply agree_map_ext=> y' /=.
-  * by rewrite -icmra_map_compose; apply icmra_map_ext=> m /=.
+  * by rewrite -ifunctor_map_compose; apply ifunctor_map_ext=> m /=.
 Qed.
-Lemma res_map_ext {Σ A B} (f g : A -n> B) :
-  (∀ r, f r ≡ g r) -> ∀ r : res Σ A, res_map f r ≡ res_map g r.
+Lemma res_map_ext {Λ Σ A B} (f g : A -n> B) (r : res Λ Σ A) :
+  (∀ x, f x ≡ g x) → res_map f r ≡ res_map g r.
 Proof.
-  move=>H r. split; simpl;
-    [apply map_fmap_setoid_ext; intros; apply agree_map_ext | | apply icmra_map_ext]; done.
+  intros Hfg; split; simpl; auto.
+  * by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
+  * by apply ifunctor_map_ext.
 Qed.
-Definition resRA_map {Σ A B} (f : A -n> B) : resRA Σ A -n> resRA Σ B :=
-  CofeMor (res_map f : resRA Σ A → resRA Σ B).
-Instance res_map_cmra_monotone {Σ} {A B : cofeT} (f : A -n> B) :
-  CMRAMonotone (@res_map Σ _ _ f).
+Definition resRA_map {Λ Σ A B} (f : A -n> B) : resRA Λ Σ A -n> resRA Λ Σ B :=
+  CofeMor (res_map f : resRA Λ Σ A → resRA Λ Σ B).
+Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) :
+  CMRAMonotone (@res_map Λ Σ _ _ f).
 Proof.
   split.
   * by intros n r1 r2; rewrite !res_includedN;
       intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
   * by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
 Qed.
-Lemma resRA_map_ne {Σ A B} (f g : A -n> B) n :
-  f ={n}= g → resRA_map (Σ := Σ) f ={n}= resRA_map g.
+Instance resRA_map_ne {Λ Σ A B} n :
+  Proper (dist n ==> dist n) (@resRA_map Λ Σ A B).
 Proof.
-  intros ? r. split; simpl;
-    [apply (mapRA_map_ne _ (agreeRA_map f) (agreeRA_map g)), agreeRA_map_ne
-     | | apply icmra_map_ne]; done.
+  intros f g Hfg r; split; simpl; auto.
+  * by apply (mapRA_map_ne _ (agreeRA_map f) (agreeRA_map g)), agreeRA_map_ne.
+  * by apply ifunctor_map_ne.
 Qed.
diff --git a/iris/tests.v b/iris/tests.v
index 77b46203ca40e7aec1a09b1574417c93c70b759f..6c03babaa8e1bc7ed78de3fea7e3ee6a6d5ed798 100644
--- a/iris/tests.v
+++ b/iris/tests.v
@@ -2,5 +2,6 @@
 Require Import iris.model.
 
 Module ModelTest. (* Make sure we got the notations right. *)
-  Definition iResTest (Σ : iParam) (w : iWld Σ) (p : iPst Σ) (g : iGst Σ) : iRes Σ := Res w p g.
+  Definition iResTest {Λ : language} {Σ : iFunctor}
+    (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p g.
 End ModelTest.
diff --git a/iris/viewshifts.v b/iris/viewshifts.v
index 79f2e4d46efe29322b5bc5b1aab9d38410fa8aa2..7e6b3640f8ffd1f0e4b77c9c73a7a7e303b201bf 100644
--- a/iris/viewshifts.v
+++ b/iris/viewshifts.v
@@ -1,9 +1,9 @@
 Require Export iris.pviewshifts.
 
-Definition vs {Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
+Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
   (□ (P → pvs E1 E2 Q))%I.
-Arguments vs {_} _ _ _%I _%I.
-Instance: Params (@vs) 3.
+Arguments vs {_ _} _ _ _%I _%I.
+Instance: Params (@vs) 4.
 Notation "P >{ E1 , E2 }> Q" := (vs E1 E2 P%I Q%I)
   (at level 69, E1 at level 1, format "P  >{ E1 , E2 }>  Q") : uPred_scope.
 Notation "P >{ E1 , E2 }> Q" := (True ⊑ vs E1 E2 P%I Q%I)
@@ -14,9 +14,9 @@ Notation "P >{ E }> Q" := (True ⊑ vs E E P%I Q%I)
   (at level 69, E at level 1, format "P  >{ E }>  Q") : C_scope.
 
 Section vs.
-Context {Σ : iParam}.
-Implicit Types P Q : iProp Σ.
-Implicit Types m : iGst Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P Q : iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 Import uPred.
 
 Lemma vs_alt E1 E2 P Q : (P ⊑ pvs E1 E2 Q) → P >{E1,E2}> Q.
@@ -25,14 +25,15 @@ Proof.
   by rewrite always_const (right_id _ _).
 Qed.
 Global Instance vs_ne E1 E2 n :
-  Proper (dist n ==> dist n ==> dist n) (@vs Σ E1 E2).
+  Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
 Proof. by intros P P' HP Q Q' HQ; rewrite /vs HP HQ. Qed.
-Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Σ E1 E2).
+Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ E1 E2).
 Proof. apply ne_proper_2, _. Qed.
 Lemma vs_mono E1 E2 P P' Q Q' :
   P ⊑ P' → Q' ⊑ Q → P' >{E1,E2}> Q' ⊑ P >{E1,E2}> Q.
 Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
-Global Instance vs_mono' E1 E2: Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@vs Σ E1 E2).
+Global Instance vs_mono' E1 E2 :
+  Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@vs Λ Σ E1 E2).
 Proof. by intros until 2; apply vs_mono. Qed.
 
 Lemma vs_false_elim E1 E2 P : False >{E1,E2}> P.
@@ -85,7 +86,7 @@ Proof.
   intros; rewrite -{1}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of.
   apply vs_close.
 Qed.
-Lemma vs_updateP E m (P : iGst Σ → Prop) :
+Lemma vs_updateP E m (P : iGst Λ Σ → Prop) :
   m ⇝: P → ownG m >{E}> (∃ m', ■ P m' ∧ ownG m').
 Proof. by intros; apply vs_alt, pvs_updateP. Qed.
 Lemma vs_update E m m' : m ⇝ m' → ownG m >{E}> ownG m'.
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index 6c7d9a87f6567692b1396f079190a97ff2601264..8acb0c293e52bf5418b902ff8bf7b240a0a2e66e 100644
--- a/iris/weakestpre.v
+++ b/iris/weakestpre.v
@@ -7,8 +7,8 @@ Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
   solve_validN.
 
-Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → iRes Σ → Prop)
-    (k : nat) (rf : iRes Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
+Record wp_go {Λ Σ} (E : coPset) (Q Qfork : expr Λ → nat → iRes Λ Σ → Prop)
+    (k : nat) (rf : iRes Λ Σ) (e1 : expr Λ) (σ1 : state Λ) := {
   wf_safe : reducible e1 σ1;
   wp_step e2 σ2 ef :
     prim_step e1 σ1 e2 σ2 ef →
@@ -17,8 +17,8 @@ Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ → nat → iRes Σ → Prop)
       Q e2 k r2 ∧
       ∀ e', ef = Some e' → Qfork e' k r2'
 }.
-CoInductive wp_pre {Σ} (E : coPset)
-     (Q : ival Σ → iProp Σ) : iexpr Σ → nat → iRes Σ → Prop :=
+CoInductive wp_pre {Λ Σ} (E : coPset)
+     (Q : val Λ → iProp Λ Σ) : expr Λ → nat → iRes Λ Σ → Prop :=
   | wp_pre_value n r v : Q v n r → wp_pre E Q (of_val v) n r
   | wp_pre_step n r1 e1 :
      to_val e1 = None →
@@ -28,38 +28,38 @@ CoInductive wp_pre {Σ} (E : coPset)
        wp_go (E ∪ Ef) (wp_pre E Q)
                       (wp_pre coPset_all (λ _, True%I)) k rf e1 σ1) →
      wp_pre E Q e1 n r1.
-Program Definition wp {Σ} (E : coPset) (e : iexpr Σ)
-  (Q : ival Σ → iProp Σ) : iProp Σ := {| uPred_holds := wp_pre E Q e |}.
+Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
+  (Q : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Q e |}.
 Next Obligation.
-  intros Σ E e Q r1 r2 n Hwp Hr.
+  intros Λ Σ E e Q r1 r2 n Hwp Hr.
   destruct Hwp as [|n r1 e2 ? Hgo]; constructor; rewrite -?Hr; auto.
   intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver.
 Qed.
 Next Obligation.
-  intros Σ E e Q r; destruct (to_val e) as [v|] eqn:?.
+  intros Λ Σ E e Q r; destruct (to_val e) as [v|] eqn:?.
   * by rewrite -(of_to_val e v) //; constructor.
   * constructor; auto with lia.
 Qed.
 Next Obligation.
-  intros Σ E e Q r1 r2 n1; revert Q E e r1 r2.
+  intros Λ Σ E e Q r1 r2 n1; revert Q E e r1 r2.
   induction n1 as [n1 IH] using lt_wf_ind; intros Q E e r1 r1' n2.
   destruct 1 as [|n1 r1 e1 ? Hgo].
   * constructor; eauto using uPred_weaken.
   * intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???].
     destruct (Hgo (rf' ⋅ rf) k Ef σ1) as [Hsafe Hstep];
-      rewrite ?(associative _) -?Hr; auto; constructor; [done|].
+      rewrite ?associative -?Hr; auto; constructor; [done|].
     intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-    exists r2, (r2' â‹… rf'); split_ands; eauto 10 using (IH k), @ra_included_l.
-    by rewrite -!(associative _) (associative _ r2).
+    exists r2, (r2' â‹… rf'); split_ands; eauto 10 using (IH k), cmra_included_l.
+    by rewrite -!associative (associative _ r2).
 Qed.
-Instance: Params (@wp) 3.
+Instance: Params (@wp) 4.
 
 Section wp.
-Context {Σ : iParam}.
-Implicit Types P : iProp Σ.
-Implicit Types Q : ival Σ → iProp Σ.
-Implicit Types v : ival Σ.
-Implicit Types e : iexpr Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P : iProp Λ Σ.
+Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
 Transparent uPred_holds.
 
 Lemma wp_weaken E1 E2 e Q1 Q2 r n n' :
@@ -70,17 +70,17 @@ Proof.
   destruct 3 as [|n' r e1 ? Hgo]; constructor; eauto.
   intros rf k Ef σ1 ???.
   assert (E2 ∪ Ef = E1 ∪ (E2 ∖ E1 ∪ Ef)) as HE'.
-  { by rewrite (associative_L _) -union_difference_L. }
+  { by rewrite associative_L -union_difference_L. }
   destruct (Hgo rf k ((E2 ∖ E1) ∪ Ef) σ1) as [Hsafe Hstep]; rewrite -?HE'; auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
   exists r2, r2'; split_ands; [rewrite HE'|eapply IH|]; eauto.
 Qed.
 Global Instance wp_ne E e n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (wp E e).
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
 Proof. by intros Q Q' HQ; split; apply wp_weaken with n; try apply HQ. Qed.
 Global Instance wp_proper E e :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (wp E e).
+  Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ E e).
 Proof.
   by intros Q Q' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
@@ -143,7 +143,7 @@ Proof.
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
   exists (r2 â‹… rR), r2'; split_ands; auto.
   * by rewrite -(associative _ r2)
-      (commutative _ rR) !(associative _) -(associative _ _ rR).
+      (commutative _ rR) !associative -(associative _ _ rR).
   * apply IH; eauto using uPred_weaken.
 Qed.
 Lemma wp_frame_later_r E e Q R :
@@ -157,7 +157,7 @@ Proof.
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
   exists (r2 â‹… rR), r2'; split_ands; auto.
   * by rewrite -(associative _ r2)
-      (commutative _ rR) !(associative _) -(associative _ _ rR).
+      (commutative _ rR) !associative -(associative _ _ rR).
   * apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
     eapply uPred_weaken with rR n; eauto.
 Qed.
@@ -180,15 +180,10 @@ Qed.
 Opaque uPred_holds.
 Import uPred.
 Global Instance wp_mono' E e :
-  Proper (pointwise_relation _ (⊑) ==> (⊑)) (wp E e).
+  Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e).
 Proof. by intros Q Q' ?; apply wp_mono. Qed.
-Lemma wp_value' E Q e v : 
-  to_val e = Some v →
-  Q v ⊑ wp E e Q.
-Proof.
-  intros Hv. apply of_to_val in Hv.
-  rewrite -Hv. by apply wp_value.
-Qed.
+Lemma wp_value' E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
+Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value. Qed.
 Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
 Proof. setoid_rewrite (commutative _ R); apply wp_frame_r. Qed.
 Lemma wp_frame_later_l E e Q R :
@@ -209,5 +204,5 @@ Proof.
   by rewrite always_elim (forall_elim v) impl_elim_l.
 Qed.
 Lemma wp_impl_r E e Q1 Q2 : (wp E e Q1 ∧ □ ∀ v, Q1 v → Q2 v) ⊑ wp E e Q2.
-Proof. by rewrite (commutative _) wp_impl_l. Qed.
+Proof. by rewrite commutative wp_impl_l. Qed.
 End wp.
diff --git a/iris/wsat.v b/iris/wsat.v
index 7a8a38e5181da22e371aef8ca5f229de41ccc52a..6281065b6a427ef6deea4d4c9dcc4e99f2338b80 100644
--- a/iris/wsat.v
+++ b/iris/wsat.v
@@ -1,11 +1,12 @@
 Require Export iris.model prelude.co_pset.
+Require Export modures.cmra_big_op modures.cmra_tactics.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 10 (✓{_} _) => solve_validN.
 Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.
 Local Hint Extern 1 (✓{_} (wld _)) => apply wld_validN.
 
-Record wsat_pre {Σ} (n : nat) (E : coPset)
-    (σ : istate Σ) (rs : gmap positive (iRes Σ)) (r : iRes Σ) := {
+Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
+    (σ : state Λ) (rs : gmap positive (iRes Λ Σ)) (r : iRes Λ Σ) := {
   wsat_pre_valid : ✓{S n} r;
   wsat_pre_state : pst r ≡ Excl σ;
   wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i);
@@ -14,31 +15,33 @@ Record wsat_pre {Σ} (n : nat) (E : coPset)
     wld r !! i ={S n}= Some (to_agree (Later (iProp_unfold P))) →
     ∃ r', rs !! i = Some r' ∧ P n r'
 }.
-Arguments wsat_pre_valid {_ _ _ _ _ _} _.
-Arguments wsat_pre_state {_ _ _ _ _ _} _.
-Arguments wsat_pre_dom {_ _ _ _ _ _} _ _ _.
-Arguments wsat_pre_wld {_ _ _ _ _ _} _ _ _ _ _.
+Arguments wsat_pre_valid {_ _ _ _ _ _ _} _.
+Arguments wsat_pre_state {_ _ _ _ _ _ _} _.
+Arguments wsat_pre_dom {_ _ _ _ _ _ _} _ _ _.
+Arguments wsat_pre_wld {_ _ _ _ _ _ _} _ _ _ _ _.
 
-Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : iRes Σ) : Prop :=
+Definition wsat {Λ Σ}
+  (n : nat) (E : coPset) (σ : state Λ) (r : iRes Λ Σ) : Prop :=
   match n with 0 => True | S n => ∃ rs, wsat_pre n E σ rs (r ⋅ big_opM rs) end.
-Instance: Params (@wsat) 4.
+Instance: Params (@wsat) 5.
 Arguments wsat : simpl never.
 
 Section wsat.
-Context {Σ : iParam}.
-Implicit Types σ : istate Σ.
-Implicit Types r : iRes Σ.
-Implicit Types rs : gmap positive (iRes Σ).
-Implicit Types P : iProp Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types σ : state Λ.
+Implicit Types r : iRes Λ Σ.
+Implicit Types rs : gmap positive (iRes Λ Σ).
+Implicit Types P : iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 
-Instance wsat_ne' : Proper (dist n ==> impl) (wsat (Σ:=Σ) n E σ).
+Instance wsat_ne' : Proper (dist n ==> impl) (@wsat Λ Σ n E σ).
 Proof.
   intros [|n] E σ r1 r2 Hr; first done; intros [rs [Hdom Hv Hs Hinv]].
   exists rs; constructor; intros until 0; setoid_rewrite <-Hr; eauto.
 Qed.
-Global Instance wsat_ne n : Proper (dist n ==> iff) (wsat (Σ:=Σ) n E σ) | 1.
+Global Instance wsat_ne n : Proper (dist n ==> iff) (@wsat Λ Σ n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed.
-Global Instance wsat_proper n : Proper ((≡) ==> iff) (wsat (Σ:=Σ) n E σ) | 1.
+Global Instance wsat_proper n : Proper ((≡) ==> iff) (@wsat Λ Σ n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed.
 Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r.
 Proof.
@@ -60,8 +63,8 @@ Proof.
 Qed.
 Lemma wsat_valid n E σ r : wsat n E σ r → ✓{n} r.
 Proof.
-  destruct n; [intros; apply cmra_valid_0|intros [rs ?]].
-  eapply cmra_valid_op_l, wsat_pre_valid; eauto.
+  destruct n; [done|intros [rs ?]].
+  eapply cmra_validN_op_l, wsat_pre_valid; eauto.
 Qed.
 Lemma wsat_init k E σ m : ✓{S k} m → wsat (S k) E σ (Res ∅ (Excl σ) m).
 Proof.
@@ -70,7 +73,7 @@ Proof.
     split_ands'; try (apply cmra_valid_validN, ra_empty_valid);
       constructor || apply Hv.
   * by intros i; rewrite lookup_empty=>-[??].
-  * intros i P ?; rewrite /= (left_id _ _) lookup_empty; inversion_clear 1.
+  * intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
 Qed.
 Lemma wsat_open n E σ r i P :
   wld r !! i ={S n}= Some (to_agree (Later (iProp_unfold P))) → i ∉ E →
@@ -79,7 +82,7 @@ Proof.
   intros HiP Hi [rs [Hval Hσ HE Hwld]].
   destruct (Hwld i P) as (rP&?&?); [solve_elem_of +|by apply lookup_wld_op_l|].
   assert (rP ⋅ r ⋅ big_opM (delete i rs) ≡ r ⋅ big_opM rs) as Hr.
-  { by rewrite (commutative _ rP) -(associative _) big_opM_delete. }
+  { by rewrite (commutative _ rP) -associative big_opM_delete. }
   exists rP; split; [exists (delete i rs); constructor; rewrite ?Hr|]; auto.
   * intros j; rewrite lookup_delete_is_Some Hr.
     generalize (HE j); solve_elem_of +Hi.
@@ -94,7 +97,7 @@ Proof.
   intros HiP HiE [rs [Hval Hσ HE Hwld]] ?.
   assert (rs !! i = None) by (apply eq_None_not_Some; naive_solver).
   assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
-  { by rewrite (commutative _ rP) -(associative _) big_opM_insert. }
+  { by rewrite (commutative _ rP) -associative big_opM_insert. }
   exists (<[i:=rP]>rs); constructor; rewrite ?Hr; auto.
   * intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
     + rewrite !lookup_op HiP !op_is_Some; solve_elem_of -.
@@ -113,15 +116,15 @@ Lemma wsat_update_pst n E σ1 σ1' r rf :
 Proof.
   intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in *.
   assert (pst rf ⋅ pst (big_opM rs) = ∅) as Hpst'.
-  { by apply: (excl_validN_inv_l n σ1); rewrite -Hpst_r (associative _). }
+  { by apply: (excl_validN_inv_l n σ1); rewrite -Hpst_r associative. }
   assert (σ1' = σ1) as ->.
   { apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
     apply (injective Excl).
-    by rewrite -Hpst_r -Hpst -(associative _) Hpst' (right_id _). }
+    by rewrite -Hpst_r -Hpst -associative Hpst' (right_id _). }
   split; [done|exists rs].
-  by constructor; split_ands'; try (rewrite /= -(associative _) Hpst').
+  by constructor; split_ands'; try (rewrite /= -associative Hpst').
 Qed.
-Lemma wsat_update_gst n E σ r rf m1 (P : iGst Σ → Prop) :
+Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) :
   m1 ≼{S n} gst r → m1 ⇝: P →
   wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
 Proof.
@@ -148,24 +151,24 @@ Proof.
   { apply eq_None_not_Some=>?; destruct (HE i) as [_ Hri']; auto; revert Hri'.
     rewrite /= !lookup_op !op_is_Some -!not_eq_None_Some; tauto. }
   assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
-  { by rewrite (commutative _ rP) -(associative _) big_opM_insert. }
+  { by rewrite (commutative _ rP) -associative big_opM_insert. }
   exists i; split_ands; [exists (<[i:=rP]>rs); constructor| |]; auto.
-  * destruct Hval as (?&?&?);  rewrite -(associative _) Hr.
-    split_ands'; rewrite /= ?(left_id _ _); [|eauto|eauto].
+  * destruct Hval as (?&?&?);  rewrite -associative Hr.
+    split_ands'; rewrite /= ?left_id; [|eauto|eauto].
     intros j; destruct (decide (j = i)) as [->|].
     + by rewrite !lookup_op Hri HrPi Hrsi !(right_id _ _) lookup_singleton.
     + by rewrite lookup_op lookup_singleton_ne // (left_id _ _).
-  * by rewrite -(associative _) Hr /= (left_id _ _).
-  * intros j; rewrite -(associative _) Hr; destruct (decide (j = i)) as [->|].
+  * by rewrite -associative Hr /= left_id.
+  * intros j; rewrite -associative Hr; destruct (decide (j = i)) as [->|].
     + rewrite /= !lookup_op lookup_singleton !op_is_Some; solve_elem_of +Hi.
     + rewrite lookup_insert_ne //.
-      rewrite lookup_op lookup_singleton_ne // (left_id _ _); eauto.
-  * intros j P'; rewrite -(associative _) Hr; destruct (decide (j=i)) as [->|].
-    + rewrite /= !lookup_op Hri HrPi Hrsi (right_id _ _) lookup_singleton=>? HP.
+      rewrite lookup_op lookup_singleton_ne // left_id; eauto.
+  * intros j P'; rewrite -associative Hr; destruct (decide (j=i)) as [->|].
+    + rewrite /= !lookup_op Hri HrPi Hrsi right_id lookup_singleton=>? HP.
       apply (injective Some), (injective to_agree),
         (injective Later), (injective iProp_unfold) in HP.
       exists rP; rewrite lookup_insert; split; [|apply HP]; auto.
-    + rewrite /= lookup_op lookup_singleton_ne // (left_id _ _)=> ??.
+    + rewrite /= lookup_op lookup_singleton_ne // left_id=> ??.
       destruct (Hwld j P') as [r' ?]; auto.
       by exists r'; rewrite lookup_insert_ne.
 Qed.
diff --git a/modures/agree.v b/modures/agree.v
index 212be59d339a148b11c1dc3c4f0392cec6fa5bc5..bceadd5189d4bc01d34855af417e1727f20a3fbc 100644
--- a/modures/agree.v
+++ b/modures/agree.v
@@ -19,7 +19,6 @@ Instance agree_validN : ValidN (agree A) := λ n x,
 Lemma agree_valid_le (x : agree A) n n' :
   agree_is_valid x n → n' ≤ n → agree_is_valid x n'.
 Proof. induction 2; eauto using agree_valid_S. Qed.
-Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
 Instance agree_equiv : Equiv (agree A) := λ x y,
   (∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧
   (∀ n, agree_is_valid x n → x n ={n}= y n).
diff --git a/modures/auth.v b/modures/auth.v
index a860a0b9b9ef63475de6e81c9c0dc51cf893e4f7..9096b46a9ad3efc112a4491c22603626c0ba7ad8 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -1,5 +1,4 @@
 Require Export modures.excl.
-Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
@@ -57,13 +56,6 @@ Section cmra.
 Context {A : cmraT}.
 
 Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
-Instance auth_valid : Valid (auth A) := λ x,
-  match authoritative x with
-  | Excl a => own x ≼ a ∧ ✓ a
-  | ExclUnit => ✓ (own x)
-  | ExclBot => False
-  end.
-Global Arguments auth_valid !_ /.
 Instance auth_validN : ValidN (auth A) := λ n x,
   match authoritative x with
   | Excl a => own x ≼{n} a ∧ ✓{n} a
@@ -92,7 +84,7 @@ Qed.
 Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} (authoritative x).
 Proof. by destruct x as [[]]. Qed.
 Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} (own x).
-Proof. destruct x as [[]]; naive_solver eauto using cmra_valid_includedN. Qed.
+Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
 
 Definition auth_cmra_mixin : CMRAMixin (auth A).
 Proof.
@@ -104,20 +96,17 @@ Proof.
   * by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
       split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
   * by intros [[] ?]; simpl.
-  * intros n [[] ?] ?; naive_solver eauto using cmra_included_S, cmra_valid_S.
-  * destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN
-      ?cmra_valid_validN; [naive_solver|naive_solver|].
-    split; [done|intros Hn; discriminate (Hn 1)].
-  * by split; simpl; rewrite (associative _).
-  * by split; simpl; rewrite (commutative _).
-  * by split; simpl; rewrite ?(ra_unit_l _).
-  * by split; simpl; rewrite ?(ra_unit_idempotent _).
+  * intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
+  * by split; simpl; rewrite associative.
+  * by split; simpl; rewrite commutative.
+  * by split; simpl; rewrite ?cmra_unit_l.
+  * by split; simpl; rewrite ?cmra_unit_idempotent.
   * intros n ??; rewrite! auth_includedN; intros [??].
-    by split; simpl; apply cmra_unit_preserving.
+    by split; simpl; apply cmra_unit_preservingN.
   * assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
-    { intros n a b1 b2 <-; apply cmra_included_l. }
+    { intros n a b1 b2 <-; apply cmra_includedN_l. }
    intros n [[a1| |] b1] [[a2| |] b2];
-     naive_solver eauto using cmra_valid_op_l, cmra_valid_includedN.
+     naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
   * by intros n ??; rewrite auth_includedN;
       intros [??]; split; simpl; apply cmra_op_minus.
 Qed.
@@ -132,10 +121,12 @@ Proof.
 Qed.
 Canonical Structure authRA : cmraT :=
   CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin.
-Instance auth_ra_empty `{Empty A} : RAIdentity A → RAIdentity (auth A).
+Instance auth_cmra_identity `{Empty A} : CMRAIdentity A → CMRAIdentity authRA.
 Proof.
-  split; simpl; [apply ra_empty_valid|].
-  by intros x; constructor; simpl; rewrite (left_id _ _).
+  split; simpl.
+  * by apply (@cmra_empty_valid A _).
+  * by intros x; constructor; rewrite /= left_id.
+  * apply Auth_timeless; apply _.
 Qed.
 Lemma auth_frag_op (a b : A) : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
diff --git a/modures/cmra.v b/modures/cmra.v
index 39ea086c82a135ef625896f8088e57e78a7fbc1b..ed96b1f5894667589fc129f3a1ea1fb8d2586d62 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -1,33 +1,54 @@
-Require Export modures.ra modures.cofe.
+Require Export modures.cofe.
+
+Class Unit (A : Type) := unit : A → A.
+Instance: Params (@unit) 2.
+
+Class Op (A : Type) := op : A → A → A.
+Instance: Params (@op) 2.
+Infix "â‹…" := op (at level 50, left associativity) : C_scope.
+Notation "(â‹…)" := op (only parsing) : C_scope.
+
+Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
+Infix "≼" := included (at level 70) : C_scope.
+Notation "(≼)" := included (only parsing) : C_scope.
+Hint Extern 0 (?x ≼ ?y) => reflexivity.
+Instance: Params (@included) 3.
+
+Class Minus (A : Type) := minus : A → A → A.
+Instance: Params (@minus) 2.
+Infix "⩪" := minus (at level 40) : C_scope.
 
 Class ValidN (A : Type) := validN : nat → A → Prop.
 Instance: Params (@validN) 3.
 Notation "✓{ n }" := (validN n) (at level 1, format "✓{ n }").
 
+Class Valid (A : Type) := valid : A → Prop.
+Instance: Params (@valid) 2.
+Notation "✓" := valid (at level 1).
+Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x.
+
 Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ={n}= x ⋅ z.
 Notation "x ≼{ n } y" := (includedN n x y)
   (at level 70, format "x  ≼{ n }  y") : C_scope.
 Instance: Params (@includedN) 4.
 Hint Extern 0 (?x ≼{_} ?y) => reflexivity.
 
-Record CMRAMixin A
-    `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
+Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
   (* setoids *)
   mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
   mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit;
-  mixin_cmra_valid_ne n : Proper (dist n ==> impl) (✓{n});
+  mixin_cmra_validN_ne n : Proper (dist n ==> impl) (✓{n});
   mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
   (* valid *)
-  mixin_cmra_valid_0 x : ✓{0} x;
-  mixin_cmra_valid_S n x : ✓{S n} x → ✓{n} x;
-  mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
+  mixin_cmra_validN_0 x : ✓{0} x;
+  mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
   (* monoid *)
   mixin_cmra_associative : Associative (≡) (⋅);
   mixin_cmra_commutative : Commutative (≡) (⋅);
   mixin_cmra_unit_l x : unit x ⋅ x ≡ x;
   mixin_cmra_unit_idempotent x : unit (unit x) ≡ unit x;
-  mixin_cmra_unit_preserving n x y : x ≼{n} y → unit x ≼{n} unit y;
-  mixin_cmra_valid_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
+  mixin_cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y;
+  mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
   mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ={n}= y
 }.
 Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} := ∀ n x y1 y2,
@@ -42,28 +63,26 @@ Structure cmraT := CMRAT {
   cmra_compl : Compl cmra_car;
   cmra_unit : Unit cmra_car;
   cmra_op : Op cmra_car;
-  cmra_valid : Valid cmra_car;
   cmra_validN : ValidN cmra_car;
   cmra_minus : Minus cmra_car;
   cmra_cofe_mixin : CofeMixin cmra_car;
   cmra_mixin : CMRAMixin cmra_car;
   cmra_extend_mixin : CMRAExtendMixin cmra_car
 }.
-Arguments CMRAT {_ _ _ _ _ _ _ _ _} _ _ _.
+Arguments CMRAT {_ _ _ _ _ _ _ _} _ _ _.
 Arguments cmra_car : simpl never.
 Arguments cmra_equiv : simpl never.
 Arguments cmra_dist : simpl never.
 Arguments cmra_compl : simpl never.
 Arguments cmra_unit : simpl never.
 Arguments cmra_op : simpl never.
-Arguments cmra_valid : simpl never.
 Arguments cmra_validN : simpl never.
 Arguments cmra_minus : simpl never.
 Arguments cmra_cofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
 Arguments cmra_extend_mixin : simpl never.
 Add Printing Constructor cmraT.
-Existing Instances cmra_unit cmra_op cmra_valid cmra_validN cmra_minus.
+Existing Instances cmra_unit cmra_op cmra_validN cmra_minus.
 Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
 Canonical Structure cmra_cofeC.
 
@@ -75,21 +94,27 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
   Global Instance cmra_unit_ne n : Proper (dist n ==> dist n) (@unit A _).
   Proof. apply (mixin_cmra_unit_ne _ (cmra_mixin A)). Qed.
-  Global Instance cmra_valid_ne n : Proper (dist n ==> impl) (@validN A _ n).
-  Proof. apply (mixin_cmra_valid_ne _ (cmra_mixin A)). Qed.
+  Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
+  Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
   Global Instance cmra_minus_ne n :
     Proper (dist n ==> dist n ==> dist n) (@minus A _).
   Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed.
-  Lemma cmra_valid_0 x : ✓{0} x.
-  Proof. apply (mixin_cmra_valid_0 _ (cmra_mixin A)). Qed.
-  Lemma cmra_valid_S n x : ✓{S n} x → ✓{n} x.
-  Proof. apply (mixin_cmra_valid_S _ (cmra_mixin A)). Qed.
-  Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
-  Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
-  Lemma cmra_unit_preserving n x y : x ≼{n} y → unit x ≼{n} unit y.
-  Proof. apply (mixin_cmra_unit_preserving _ (cmra_mixin A)). Qed.
-  Lemma cmra_valid_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
-  Proof. apply (mixin_cmra_valid_op_l _ (cmra_mixin A)). Qed.
+  Lemma cmra_validN_0 x : ✓{0} x.
+  Proof. apply (mixin_cmra_validN_0 _ (cmra_mixin A)). Qed.
+  Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x.
+  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
+  Global Instance cmra_associative : Associative (≡) (@op A _).
+  Proof. apply (mixin_cmra_associative _ (cmra_mixin A)). Qed.
+  Global Instance cmra_commutative : Commutative (≡) (@op A _).
+  Proof. apply (mixin_cmra_commutative _ (cmra_mixin A)). Qed.
+  Lemma cmra_unit_l x : unit x ⋅ x ≡ x.
+  Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed.
+  Lemma cmra_unit_idempotent x : unit (unit x) ≡ unit x.
+  Proof. apply (mixin_cmra_unit_idempotent _ (cmra_mixin A)). Qed.
+  Lemma cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y.
+  Proof. apply (mixin_cmra_unit_preservingN _ (cmra_mixin A)). Qed.
+  Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
+  Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
   Lemma cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ={n}= y.
   Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
   Lemma cmra_extend_op n x y1 y2 :
@@ -98,22 +123,24 @@ Section cmra_mixin.
   Proof. apply (cmra_extend_mixin A). Qed.
 End cmra_mixin.
 
-Hint Extern 0 (✓{0} _) => apply cmra_valid_0.
+Hint Extern 0 (✓{0} _) => apply cmra_validN_0.
+
+(** * CMRAs with a global identity element *)
+(** We use the notation ∅ because for most instances (maps, sets, etc) the
+`empty' element is the global identity. *)
+Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := {
+  cmra_empty_valid : ✓ ∅;
+  cmra_empty_left_id :> LeftId (≡) ∅ (⋅);
+  cmra_empty_timeless :> Timeless ∅
+}.
 
 (** * Morphisms *)
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {
   includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y;
   validN_preserving n x : ✓{n} x → ✓{n} (f x)
 }.
-Instance compose_cmra_monotone {A B C : cmraT} (f : A -n> B) (g : B -n> C) :
-  CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ◎ f).
-Proof.
-  split.
-  - move=> n x y Hxy /=. eapply includedN_preserving, includedN_preserving; done.
-  - move=> n x Hx /=. eapply validN_preserving, validN_preserving; done.
-Qed.
 
-(** * Updates *)
+(** * Frame preserving updates *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
   ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
 Instance: Params (@cmra_updateP) 3.
@@ -127,41 +154,129 @@ Instance: Params (@cmra_update) 3.
 Section cmra.
 Context {A : cmraT}.
 Implicit Types x y z : A.
+Implicit Types xs ys zs : list A.
 
+(** ** Setoids *)
+Global Instance cmra_unit_proper : Proper ((≡) ==> (≡)) (@unit A _).
+Proof. apply (ne_proper _). Qed.
+Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
+Proof.
+  intros x1 x2 Hx y1 y2 Hy.
+  by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
+Qed.
+Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
+Proof. apply (ne_proper_2 _). Qed.
+Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
+Proof. by split; apply cmra_validN_ne. Qed.
+Global Instance cmra_validN_proper : Proper ((≡) ==> iff) (@validN A _ n) | 1.
+Proof. by intros n x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
+Global Instance cmra_minus_proper : Proper ((≡) ==> (≡) ==> (≡)) (@minus A _).
+Proof. apply (ne_proper_2 _). Qed.
+
+Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (@valid A _).
+Proof. by intros x y Hxy; split; intros ? n; [rewrite -Hxy|rewrite Hxy]. Qed.
+Global Instance cmra_includedN_ne n :
+  Proper (dist n ==> dist n ==> iff) (@includedN A _ _ n) | 1.
+Proof.
+  intros x x' Hx y y' Hy.
+  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
+Qed.
+Global Instance cmra_includedN_proper n :
+  Proper ((≡) ==> (≡) ==> iff) (@includedN A _ _ n) | 1.
+Proof.
+  intros x x' Hx y y' Hy; revert Hx Hy; rewrite !equiv_dist=> Hx Hy.
+  by rewrite (Hx n) (Hy n).
+Qed.
+Global Instance cmra_included_proper :
+  Proper ((≡) ==> (≡) ==> iff) (@included A _ _) | 1.
+Proof.
+  intros x x' Hx y y' Hy.
+  by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
+Qed.
+
+(** ** Validity *)
+Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
+Proof. done. Qed.
+Lemma cmra_validN_le x n n' : ✓{n} x → n' ≤ n → ✓{n'} x.
+Proof. induction 2; eauto using cmra_validN_S. Qed.
+Lemma cmra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x.
+Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed.
+Lemma cmra_validN_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y.
+Proof. rewrite (commutative _ x); apply cmra_validN_op_l. Qed.
+Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y.
+Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
+
+(** ** Units *)
+Lemma cmra_unit_r x : x ⋅ unit x ≡ x.
+Proof. by rewrite (commutative _ x) cmra_unit_l. Qed.
+Lemma cmra_unit_unit x : unit x ⋅ unit x ≡ unit x.
+Proof. by rewrite -{2}(cmra_unit_idempotent x) cmra_unit_r. Qed.
+Lemma cmra_unit_validN x n : ✓{n} x → ✓{n} (unit x).
+Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
+Lemma cmra_unit_valid x : ✓ x → ✓ (unit x).
+Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
+
+(** ** Order *)
 Lemma cmra_included_includedN x y : x ≼ y ↔ ∀ n, x ≼{n} y.
 Proof.
   split; [by intros [z Hz] n; exists z; rewrite Hz|].
   intros Hxy; exists (y ⩪ x); apply equiv_dist; intros n.
   symmetry; apply cmra_op_minus, Hxy.
 Qed.
+Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
+Proof.
+  split.
+  * by intros x; exists (unit x); rewrite cmra_unit_r.
+  * intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
+    by rewrite (associative _) -Hy -Hz.
+Qed.
+Global Instance cmra_included_preorder: PreOrder (@included A _ _).
+Proof.
+  split; red; intros until 0; rewrite !cmra_included_includedN; first done.
+  intros; etransitivity; eauto.
+Qed.
+Lemma cmra_validN_includedN x y n : ✓{n} y → x ≼{n} y → ✓{n} x.
+Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
+Lemma cmra_validN_included x y n : ✓{n} y → x ≼ y → ✓{n} x.
+Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.
+
+Lemma cmra_includedN_0 x y : x ≼{0} y.
+Proof. by exists (unit x). Qed.
+Lemma cmra_includedN_S x y n : x ≼{S n} y → x ≼{n} y.
+Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
+Lemma cmra_includedN_le x y n n' : x ≼{n} y → n' ≤ n → x ≼{n'} y.
+Proof. induction 2; auto using cmra_includedN_S. Qed.
+
+Lemma cmra_includedN_l n x y : x ≼{n} x ⋅ y.
+Proof. by exists y. Qed.
+Lemma cmra_included_l x y : x ≼ x ⋅ y.
+Proof. by exists y. Qed.
+Lemma cmra_includedN_r n x y : y ≼{n} x ⋅ y.
+Proof. rewrite (commutative op); apply cmra_includedN_l. Qed.
+Lemma cmra_included_r x y : y ≼ x ⋅ y.
+Proof. rewrite (commutative op); apply cmra_included_l. Qed.
 
-Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (✓{n} : A → _) | 1.
-Proof. by split; apply cmra_valid_ne. Qed.
-Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (✓{n} : A → _) | 1.
-Proof. by intros n x1 x2 Hx; apply cmra_valid_ne', equiv_dist. Qed.
-Global Instance cmra_ra : RA A.
+Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
+Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed.
+Lemma cmra_included_unit x : unit x ≼ x.
+Proof. by exists x; rewrite cmra_unit_l. Qed.
+Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
+Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
+Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
+Proof. by intros; rewrite -!(commutative _ z); apply cmra_preserving_l. Qed.
+
+Lemma cmra_included_dist_l x1 x2 x1' n :
+  x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2.
 Proof.
-  split; try by (destruct (@cmra_mixin A);
-    eauto using ne_proper, ne_proper_2 with typeclass_instances).
-  * by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite -Hx.
-  * intros x y; rewrite !cmra_included_includedN.
-    eauto using @cmra_unit_preserving.
-  * intros x y; rewrite !cmra_valid_validN; intros ? n.
-    by apply cmra_valid_op_l with y.
-  * intros x y [z Hz]; apply equiv_dist; intros n.
-    by apply cmra_op_minus; exists z; rewrite Hz.
+  intros [z Hx2] Hx1; exists (x1' â‹… z); split; auto using cmra_included_l.
+  by rewrite Hx1 Hx2.
 Qed.
-Lemma cmra_valid_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y.
-Proof. rewrite (commutative _ x); apply cmra_valid_op_l. Qed.
-Lemma cmra_valid_le x n n' : ✓{n} x → n' ≤ n → ✓{n'} x.
-Proof. induction 2; eauto using cmra_valid_S. Qed.
-Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (@op A _).
+
+(** ** Minus *)
+Lemma cmra_op_minus' x y : x ≼ y → x ⋅ y ⩪ x ≡ y.
 Proof.
-  intros x1 x2 Hx y1 y2 Hy.
-  by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
+  rewrite cmra_included_includedN equiv_dist; eauto using cmra_op_minus.
 Qed.
-Lemma cmra_unit_valid x n : ✓{n} x → ✓{n} (unit x).
-Proof. rewrite -{1}(ra_unit_l x); apply cmra_valid_op_l. Qed.
 
 (** ** Timeless *)
 Lemma cmra_timeless_included_l x y : Timeless x → ✓{1} y → x ≼{1} y → x ≼ y.
@@ -177,68 +292,24 @@ Lemma cmra_op_timeless x1 x2 :
 Proof.
   intros ??? z Hz.
   destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
-  { by rewrite -?Hz; apply cmra_valid_validN. }
+  { by rewrite -?Hz. }
   by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
 Qed.
 
-(** ** Order *)
-Global Instance cmra_included_ne n :
-  Proper (dist n ==> dist n ==> iff) (includedN n : relation A) | 1.
-Proof.
-  intros x x' Hx y y' Hy; unfold includedN.
-  by setoid_rewrite Hx; setoid_rewrite Hy.
-Qed.
-Global Instance cmra_included_proper : 
-  Proper ((≡) ==> (≡) ==> iff) (includedN n : relation A) | 1.
-Proof.
-  intros n x x' Hx y y' Hy; unfold includedN.
-  by setoid_rewrite Hx; setoid_rewrite Hy.
-Qed.
-Lemma cmra_included_0 x y : x ≼{0} y.
-Proof. by exists (unit x). Qed.
-Lemma cmra_included_S x y n : x ≼{S n} y → x ≼{n} y.
-Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
-Lemma cmra_included_le x y n n' : x ≼{n} y → n' ≤ n → x ≼{n'} y.
-Proof. induction 2; auto using cmra_included_S. Qed.
+(** ** RAs with an empty element *)
+Section identity.
+  Context `{Empty A, !CMRAIdentity A}.
+  Lemma cmra_empty_leastN  n x : ∅ ≼{n} x.
+  Proof. by exists x; rewrite left_id. Qed.
+  Lemma cmra_empty_least x : ∅ ≼ x.
+  Proof. by exists x; rewrite left_id. Qed.
+  Global Instance cmra_empty_right_id : RightId (≡) ∅ (⋅).
+  Proof. by intros x; rewrite (commutative op) left_id. Qed.
+  Lemma cmra_unit_empty : unit ∅ ≡ ∅.
+  Proof. by rewrite -{2}(cmra_unit_l ∅) right_id. Qed.
+End identity.
 
-Lemma cmra_included_l n x y : x ≼{n} x ⋅ y.
-Proof. by exists y. Qed.
-Lemma cmra_included_r n x y : y ≼{n} x ⋅ y.
-Proof. rewrite (commutative op); apply cmra_included_l. Qed.
-Global Instance cmra_included_ord n : PreOrder (includedN n : relation A).
-Proof.
-  split.
-  * by intros x; exists (unit x); rewrite ra_unit_r.
-  * intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
-    by rewrite (associative _) -Hy -Hz.
-Qed.
-Lemma cmra_valid_includedN x y n : ✓{n} y → x ≼{n} y → ✓{n} x.
-Proof. intros Hyv [z ?]; cofe_subst y; eauto using @cmra_valid_op_l. Qed.
-Lemma cmra_valid_included x y n : ✓{n} y → x ≼ y → ✓{n} x.
-Proof. rewrite cmra_included_includedN; eauto using @cmra_valid_includedN. Qed.
-Lemma cmra_included_dist_l x1 x2 x1' n :
-  x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2.
-Proof.
-  intros [z Hx2] Hx1; exists (x1' â‹… z); split; auto using ra_included_l.
-  by rewrite Hx1 Hx2.
-Qed.
-
-(** ** RAs with empty element *)
-Lemma cmra_empty_least `{Empty A, !RAIdentity A} n x : ∅ ≼{n} x.
-Proof. by exists x; rewrite (left_id _ _). Qed.
-
-(** ** big ops *)
-Section bigop.
-  Context `{Empty A, !RAIdentity A, FinMap K M}.
-  Lemma big_opM_lookup_valid n m i x :
-    ✓{n} (big_opM m) → m !! i = Some x → ✓{n} x.
-  Proof.
-    intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
-    apply cmra_valid_op_l.
-  Qed.
-End bigop.
-
-(** ** Properties of [(⇝)] relation *)
+(** ** Updates *)
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
 Lemma cmra_update_updateP x y : x ⇝ y ↔ x ⇝: (y =).
@@ -249,59 +320,70 @@ Proof.
 Qed.
 End cmra.
 
-Hint Resolve cmra_ra.
-Hint Extern 0 (_ ≼{0} _) => apply cmra_included_0.
-(* Also via [cmra_cofe; cofe_equivalence] *)
-Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances.
-
-(* Solver for validity *)
-Ltac solve_validN :=
-  match goal with
-  | H : ✓{?n} ?y |- ✓{?n'} ?x =>
-     let Hn := fresh in let Hx := fresh in
-     assert (n' ≤ n) as Hn by omega;
-     assert (x ≼ y) as Hx by solve_included;
-     eapply cmra_valid_le, Hn; eapply cmra_valid_included, Hx; apply H
-  end.
+Hint Extern 0 (_ ≼{0} _) => apply cmra_includedN_0.
 
+(** * Properties about monotone functions *)
 Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
 Proof. by split. Qed.
-Instance cmra_monotone_ra_monotone {A B : cmraT} (f : A → B) :
-  CMRAMonotone f → RAMonotone f.
+Instance cmra_monotone_compose {A B C : cmraT} (f : A → B) (g : B → C) :
+  CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ∘ f).
 Proof.
   split.
-  * intros x y; rewrite !cmra_included_includedN.
-    by intros ? n; apply includedN_preserving.
-  * intros x; rewrite !cmra_valid_validN.
-    by intros ? n; apply validN_preserving.
+  * move=> n x y Hxy /=. by apply includedN_preserving, includedN_preserving.
+  * move=> n x Hx /=. by apply validN_preserving, validN_preserving.
 Qed.
 
-(** Discrete *)
+Section cmra_monotone.
+  Context {A B : cmraT} (f : A → B) `{!CMRAMonotone f}.
+  Lemma included_preserving x y : x ≼ y → f x ≼ f y.
+  Proof.
+    rewrite !cmra_included_includedN; eauto using includedN_preserving.
+  Qed.
+  Lemma valid_preserving x : ✓ x → ✓ (f x).
+  Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
+End cmra_monotone.
+
+(** * Instances *)
+(** ** Discrete CMRA *)
+Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
+  (* setoids *)
+  ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x);
+  ra_unit_ne :> Proper ((≡) ==> (≡)) unit;
+  ra_validN_ne :> Proper ((≡) ==> impl) ✓;
+  ra_minus_ne :> Proper ((≡) ==> (≡) ==> (≡)) minus;
+  (* monoid *)
+  ra_associative :> Associative (≡) (⋅);
+  ra_commutative :> Commutative (≡) (⋅);
+  ra_unit_l x : unit x ⋅ x ≡ x;
+  ra_unit_idempotent x : unit (unit x) ≡ unit x;
+  ra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
+  ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x;
+  ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
+}.
+
 Section discrete.
-  Context `{ra : RA A}.
-  Existing Instances discrete_dist discrete_compl.
+  Context {A : cofeT} `{∀ x : A, Timeless x}.
+  Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
+
   Instance discrete_validN : ValidN A := λ n x,
     match n with 0 => True | S n => ✓ x end.
   Definition discrete_cmra_mixin : CMRAMixin A.
   Proof.
-    split; try by (destruct ra; auto).
-    * by intros [|n]; try apply ra_op_proper.
-    * by intros [|n]; try apply ra_unit_proper.
-    * by intros [|n]; try apply ra_valid_proper.
-    * by intros [|n]; try apply ra_minus_proper.
-    * by intros [|n].
-    * intros x; split; intros Hvalid. by intros [|n]. apply (Hvalid 1).
-    * by intros [|n]; try apply ra_unit_preserving.
-    * by intros [|n]; try apply ra_valid_op_l.
-    * by intros [|n] x y; try apply ra_op_minus.
+    destruct ra; split; unfold Proper, respectful, includedN;
+      repeat match goal with
+      | |- ∀ n : nat, _ => intros [|?]
+      end; try setoid_rewrite <-(timeless_S _ _ _ _); try done.
+    by intros x y ?; exists x.
   Qed.
   Definition discrete_extend_mixin : CMRAExtendMixin A.
   Proof.
-    intros [|n] x y1 y2 ??; [|by exists (y1,y2); rewrite /dist /discrete_dist].
-    by exists (x,unit x); simpl; rewrite ra_unit_r.
+    intros [|n] x y1 y2 ??.
+    * by exists (unit x, x); rewrite /= ra_unit_l.
+    * exists (y1,y2); split_ands; auto.
+      apply (timeless _), dist_le with (S n); auto with lia.
   Qed.
   Definition discreteRA : cmraT :=
-    CMRAT discrete_cofe_mixin discrete_cmra_mixin discrete_extend_mixin.
+    CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
   Lemma discrete_updateP (x : A) (P : A → Prop) `{!Inhabited (sig P)} :
     (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → (x : discreteRA) ⇝: P.
   Proof.
@@ -312,18 +394,28 @@ Section discrete.
     (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → (x : discreteRA) ⇝ y.
   Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed.
 End discrete.
-Arguments discreteRA _ {_ _ _ _ _ _}.
 
-(** CMRA for the unit type *)
-Canonical Structure unitRA : cmraT := discreteRA ().
+(** ** CMRA for the unit type *)
+Section unit.
+  Instance unit_valid : Valid () := λ x, True.
+  Instance unit_unit : Unit () := λ x, x.
+  Instance unit_op : Op () := λ x y, ().
+  Instance unit_minus : Minus () := λ x y, ().
+  Global Instance unit_empty : Empty () := ().
+  Definition unit_ra : RA ().
+  Proof. by split. Qed.
+  Canonical Structure unitRA : cmraT :=
+    Eval cbv [unitC discreteRA cofe_car] in discreteRA unit_ra.
+  Global Instance unit_cmra_identity : CMRAIdentity unitRA.
+  Proof. by split; intros []. Qed.
+End unit.
 
-(** Product *)
+(** ** Product *)
 Section prod.
   Context {A B : cmraT}.
   Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
   Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
   Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)).
-  Instance prod_valid : Valid (A * B) := λ x, ✓ (x.1) ∧ ✓ (x.2).
   Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} (x.1) ∧ ✓{n} (x.2).
   Instance prod_minus : Minus (A * B) := λ x y, (x.1 ⩪ y.1, x.2 ⩪ y.2).
   Lemma prod_included (x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
@@ -344,25 +436,18 @@ Section prod.
     * by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
     * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
         split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
-    * split; apply cmra_valid_0.
-    * by intros n x [??]; split; apply cmra_valid_S.
-    * intros x; split; [by intros [??] n; split; apply cmra_valid_validN|].
-      intros Hvalid; split; apply cmra_valid_validN; intros n; apply Hvalid.
+    * by split.
+    * by intros n x [??]; split; apply cmra_validN_S.
     * split; simpl; apply (associative _).
     * split; simpl; apply (commutative _).
-    * split; simpl; apply ra_unit_l.
-    * split; simpl; apply ra_unit_idempotent.
+    * split; simpl; apply cmra_unit_l.
+    * split; simpl; apply cmra_unit_idempotent.
     * intros n x y; rewrite !prod_includedN.
-      by intros [??]; split; apply cmra_unit_preserving.
-    * intros n x y [??]; split; simpl in *; eapply cmra_valid_op_l; eauto.
+      by intros [??]; split; apply cmra_unit_preservingN.
+    * intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
     * intros x y n; rewrite prod_includedN; intros [??].
       by split; apply cmra_op_minus.
   Qed.
-  Global Instance prod_ra_empty `{Empty A, Empty B} :
-    RAIdentity A → RAIdentity B → RAIdentity (A * B).
-  Proof.
-    repeat split; simpl; repeat (apply ra_empty_valid || apply (left_id _ _)).
-  Qed.
   Definition prod_cmra_extend_mixin : CMRAExtendMixin (A * B).
   Proof.
     intros n x y1 y2 [??] [??]; simpl in *.
@@ -372,6 +457,14 @@ Section prod.
   Qed.
   Canonical Structure prodRA : cmraT :=
     CMRAT prod_cofe_mixin prod_cmra_mixin prod_cmra_extend_mixin.
+  Global Instance prod_cmra_identity `{Empty A, Empty B} :
+    CMRAIdentity A → CMRAIdentity B → CMRAIdentity prodRA.
+  Proof.
+    split.
+    * split; apply cmra_empty_valid.
+    * by split; rewrite /=left_id.
+    * by intros ? [??]; split; apply (timeless _).
+  Qed.
 End prod.
 Arguments prodRA : clear implicits.
 
diff --git a/modures/cmra_big_op.v b/modures/cmra_big_op.v
new file mode 100644
index 0000000000000000000000000000000000000000..c96118a095d009aa0644004294360c23c4392691
--- /dev/null
+++ b/modures/cmra_big_op.v
@@ -0,0 +1,80 @@
+Require Export modures.cmra.
+Require Import prelude.fin_maps.
+
+Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
+  match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
+Arguments big_op _ _ !_ /.
+Instance: Params (@big_op) 2.
+Definition big_opM {A : cmraT} `{FinMapToList K A M, Empty A} (m : M) : A :=
+  big_op (snd <$> map_to_list m).
+Instance: Params (@big_opM) 5.
+
+(** * Properties about big ops *)
+Section big_op.
+Context `{CMRAIdentity A}.
+
+(** * Big ops *)
+Lemma big_op_nil : big_op (@nil A) = ∅.
+Proof. done. Qed.
+Lemma big_op_cons x xs : big_op (x :: xs) = x â‹… big_op xs.
+Proof. done. Qed.
+Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
+Proof.
+  induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
+  * by rewrite IH.
+  * by rewrite !(associative _) (commutative _ x).
+  * by transitivity (big_op xs2).
+Qed.
+Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
+Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
+Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
+Proof.
+  induction xs as [|x xs IH]; simpl; first by rewrite ?(left_id _ _).
+  by rewrite IH (associative _).
+Qed.
+Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys.
+Proof.
+  induction 1 as [|x xs ys|x y xs|x xs ys|xs ys zs]; rewrite //=.
+  * by apply cmra_preserving_l.
+  * by rewrite !associative (commutative _ y).
+  * by transitivity (big_op ys); last apply cmra_included_r.
+  * by transitivity (big_op ys).
+Qed.
+Lemma big_op_delete xs i x :
+  xs !! i = Some x → x ⋅ big_op (delete i xs) ≡ big_op xs.
+Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.
+
+Context `{FinMap K M}.
+Lemma big_opM_empty : big_opM (∅ : M A) ≡ ∅.
+Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
+Lemma big_opM_insert (m : M A) i x :
+  m !! i = None → big_opM (<[i:=x]> m) ≡ x ⋅ big_opM m.
+Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
+Lemma big_opM_delete (m : M A) i x :
+  m !! i = Some x → x ⋅ big_opM (delete i m) ≡ big_opM m.
+Proof.
+  intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete.
+Qed.
+Lemma big_opM_singleton i x : big_opM ({[i ↦ x]} : M A) ≡ x.
+Proof.
+  rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
+  by rewrite big_opM_empty (right_id _ _).
+Qed.
+Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : M A → _).
+Proof.
+  intros m1; induction m1 as [|i x m1 ? IH] using map_ind.
+  { by intros m2; rewrite (symmetry_iff (≡)) map_equiv_empty; intros ->. }
+  intros m2 Hm2; rewrite big_opM_insert //.
+  rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
+  destruct (map_equiv_lookup (<[i:=x]> m1) m2 i x)
+    as (y&?&Hxy); auto using lookup_insert.
+  rewrite Hxy -big_opM_insert; last auto using lookup_delete.
+  by rewrite insert_delete.
+Qed.
+Lemma big_opM_lookup_valid n m i x :
+  ✓{n} (big_opM m) → m !! i = Some x → ✓{n} x.
+Proof.
+  intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
+  apply cmra_validN_op_l.
+Qed.
+End big_op.
diff --git a/modures/cmra_tactics.v b/modures/cmra_tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..c2cce946a58e44e8b5fc5b43248471872fc56019
--- /dev/null
+++ b/modures/cmra_tactics.v
@@ -0,0 +1,66 @@
+Require Export modures.cmra.
+Require Import modures.cmra_big_op.
+
+(** * Simple solver for validity and inclusion by reflection *)
+Module ra_reflection. Section ra_reflection.
+  Context `{CMRAIdentity A}.
+
+  Inductive expr :=
+    | EVar : nat → expr
+    | EEmpty : expr
+    | EOp : expr → expr → expr.
+  Fixpoint eval (Σ : list A) (e : expr) : A :=
+    match e with
+    | EVar n => from_option ∅ (Σ !! n)
+    | EEmpty => ∅
+    | EOp e1 e2 => eval Σ e1 ⋅ eval Σ e2
+    end.
+  Fixpoint flatten (e : expr) : list nat :=
+    match e with
+    | EVar n => [n]
+    | EEmpty => []
+    | EOp e1 e2 => flatten e1 ++ flatten e2
+    end.
+  Lemma eval_flatten Σ e :
+    eval Σ e ≡ big_op ((λ n, from_option ∅ (Σ !! n)) <$> flatten e).
+  Proof.
+    by induction e as [| |e1 IH1 e2 IH2];
+      rewrite /= ?(right_id _ _) ?fmap_app ?big_op_app ?IH1 ?IH2.
+  Qed.
+  Lemma flatten_correct Σ e1 e2 :
+    flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.
+  Proof.
+    by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He.
+  Qed.
+
+  Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
+  Global Instance quote_empty: Quote E1 E1 ∅ EEmpty.
+  Global Instance quote_var Σ1 Σ2 e i:
+    rlist.QuoteLookup Σ1 Σ2 e i → Quote Σ1 Σ2 e (EVar i) | 1000.
+  Global Instance quote_app Σ1 Σ2 Σ3 x1 x2 e1 e2 :
+    Quote Σ1 Σ2 x1 e1 → Quote Σ2 Σ3 x2 e2 → Quote Σ1 Σ3 (x1 ⋅ x2) (EOp e1 e2).
+  End ra_reflection.
+
+  Ltac quote :=
+    match goal with
+    | |- @included _ _ _ ?x ?y =>
+      lazymatch type of (_ : Quote [] _ x _) with Quote _ ?Σ2 _ ?e1 =>
+      lazymatch type of (_ : Quote Σ2 _ y _) with Quote _ ?Σ3 _ ?e2 =>
+        change (eval Σ3 e1 ≼ eval Σ3 e2)
+      end end
+    end.
+End ra_reflection.
+
+Ltac solve_included :=
+  ra_reflection.quote;
+  apply ra_reflection.flatten_correct, (bool_decide_unpack _);
+  vm_compute; apply I.
+
+Ltac solve_validN :=
+  match goal with
+  | H : ✓{?n} ?y |- ✓{?n'} ?x =>
+     let Hn := fresh in let Hx := fresh in
+     assert (n' ≤ n) as Hn by omega;
+     assert (x ≼ y) as Hx by solve_included;
+     eapply cmra_validN_le, Hn; eapply cmra_validN_included, Hx; apply H
+  end.
diff --git a/modures/cofe.v b/modures/cofe.v
index b0b2de1944d7ecbd00507999da15df55d8dd316a..becd4395a9c335cf840a67d3365a311185d4ed1a 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -129,6 +129,11 @@ Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
 (** Timeless elements *)
 Class Timeless {A : cofeT} (x : A) := timeless y : x ={1}= y → x ≡ y.
 Arguments timeless {_} _ {_} _ _.
+Lemma timeless_S {A : cofeT} (x y : A) n : Timeless x → x ≡ y ↔ x ={S n}= y.
+Proof.
+  split; intros; [by apply equiv_dist|].
+  apply (timeless _), dist_le with (S n); auto with lia.
+Qed.
 
 (** Fixpoint *)
 Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
@@ -235,6 +240,8 @@ Section unit.
   Definition unit_cofe_mixin : CofeMixin unit.
   Proof. by repeat split; try exists 0. Qed.
   Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
+  Global Instance unit_timeless (x : ()) : Timeless x.
+  Proof. done. Qed.
 End unit.
 
 (** Product *)
diff --git a/modures/cofe_solver.v b/modures/cofe_solver.v
index 3ba4f641e7cb8b465acf81801c9614878596d269..977a6fdc5d6852f4986d93c370aa9cf12ad53bf8 100644
--- a/modures/cofe_solver.v
+++ b/modures/cofe_solver.v
@@ -34,7 +34,7 @@ Fixpoint A (k : nat) : cofeT :=
 Fixpoint f {k} : A k -n> A (S k) :=
   match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g,f) end
 with g {k} : A (S k) -n> A k :=
-  match k with 0 => CofeMor (λ _, () : unitC) | S k => map (f,g) end.
+  match k with 0 => CofeMor (λ _, ()) | S k => map (f,g) end.
 Definition f_S k (x : A (S k)) : f x = map (g,f) x := eq_refl.
 Definition g_S k (x : A (S (S k))) : g x = map (f,g) x := eq_refl.
 Lemma gf {k} (x : A k) : g (f x) ≡ x.
diff --git a/modures/dra.v b/modures/dra.v
index 3bf9e306a24135b777f5d026cbf55373b9ed4510..4965a1264c755c7d96c8e9cb6e30ab6888165ff1 100644
--- a/modures/dra.v
+++ b/modures/dra.v
@@ -1,4 +1,4 @@
-Require Export modures.ra modures.cmra.
+Require Export modures.cmra.
 
 (** From disjoint pcm *)
 Record validity {A} (P : A → Prop) : Type := Validity {
@@ -99,10 +99,9 @@ Program Instance validity_minus : Minus T := λ x y,
            (✓ x ∧ ✓ y ∧ validity_car y ≼ validity_car x) _.
 Solve Obligations with naive_solver auto using dra_minus_valid.
 
-Instance validity_ra : RA T.
+Definition validity_ra : RA (discreteC T).
 Proof.
   split.
-  * apply _.
   * intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
     split; intros (?&?&?); split_ands';
       first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
@@ -130,11 +129,11 @@ Proof.
   * intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
       intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
 Qed.
-Definition validityRA : cmraT := discreteRA T.
+Definition validityRA : cmraT := discreteRA validity_ra.
 Definition validity_update (x y : validityRA) :
   (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ⇝ y.
 Proof.
-  intros Hxy; apply discrete_update.
+  intros Hxy. apply discrete_update.
   intros z (?&?&?); split_ands'; try eapply Hxy; eauto.
 Qed.
 End dra.
diff --git a/modures/excl.v b/modures/excl.v
index fdb667dcf84b9ea09b76d2e150f5fac09c83868e..795c2840d1b42fcae5f20fbad07c8f8fb84a71af 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -83,8 +83,6 @@ Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
 Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
 
 (* CMRA *)
-Instance excl_valid : Valid (excl A) := λ x,
-  match x with Excl _ | ExclUnit => True | ExclBot => False end.
 Instance excl_validN : ValidN (excl A) := λ n x,
   match x with Excl _ | ExclUnit => True | ExclBot => n = 0 end.
 Global Instance excl_empty : Empty (excl A) := ExclUnit.
@@ -110,8 +108,6 @@ Proof.
   * by destruct 1; inversion_clear 1; constructor.
   * by intros [].
   * intros n [?| |]; simpl; auto with lia.
-  * intros x; split; [by intros ? [|n]; destruct x|].
-    by intros Hx; specialize (Hx 1); destruct x.
   * by intros [?| |] [?| |] [?| |]; constructor.
   * by intros [?| |] [?| |]; constructor.
   * by intros [?| |]; constructor.
@@ -120,8 +116,6 @@ Proof.
   * by intros n [?| |] [?| |].
   * by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
 Qed.
-Global Instance excl_empty_ra : RAIdentity (excl A).
-Proof. split. done. by intros []. Qed.
 Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
 Proof.
   intros [|n] x y1 y2 ? Hx; [by exists (x,∅); destruct x|].
@@ -133,6 +127,8 @@ Proof.
 Qed.
 Canonical Structure exclRA : cmraT :=
   CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
+Global Instance excl_cmra_identity : CMRAIdentity exclRA.
+Proof. split. done. by intros []. apply _. Qed.
 Lemma excl_validN_inv_l n x y : ✓{S n} (Excl x ⋅ y) → y = ∅.
 Proof. by destruct y. Qed.
 Lemma excl_validN_inv_r n x y : ✓{S n} (x ⋅ Excl y) → x = ∅.
diff --git a/modures/fin_maps.v b/modures/fin_maps.v
index 9cefea9046d7621830f881f8a96e17bae2d11385..bf289e28999a641a71b013b036ff87ea653e799f 100644
--- a/modures/fin_maps.v
+++ b/modures/fin_maps.v
@@ -50,7 +50,7 @@ Proof.
   intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
     [by constructor|by apply lookup_ne].
 Qed.
-Global Instance map_empty_timeless : Timeless (∅ : gmap K A).
+Instance map_empty_timeless : Timeless (∅ : gmap K A).
 Proof.
   intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
   inversion_clear Hm; constructor.
@@ -81,7 +81,6 @@ Context `{Countable K} {A : cmraT}.
 
 Instance map_op : Op (gmap K A) := merge op.
 Instance map_unit : Unit (gmap K A) := fmap unit.
-Instance map_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
 Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m!!i).
 Instance map_minus : Minus (gmap K A) := merge minus.
 Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
@@ -95,7 +94,7 @@ Proof.
   split.
   * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
   * intros Hm; exists (m2 ⩪ m1); intros i.
-    by rewrite lookup_op lookup_minus ra_op_minus.
+    by rewrite lookup_op lookup_minus cmra_op_minus'.
 Qed.
 Lemma map_includedN_spec (m1 m2 : gmap K A) n :
   m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
@@ -113,26 +112,18 @@ Proof.
   * by intros n m1 m2 Hm ? i; rewrite -(Hm i).
   * by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i).
   * by intros m i.
-  * intros n m Hm i; apply cmra_valid_S, Hm.
-  * intros m; split; [by intros Hm n i; apply cmra_valid_validN|].
-    intros Hm i; apply cmra_valid_validN; intros n; apply Hm.
-  * by intros m1 m2 m3 i; rewrite !lookup_op (associative _).
-  * by intros m1 m2 i; rewrite !lookup_op (commutative _).
-  * by intros m i; rewrite lookup_op !lookup_unit ra_unit_l.
-  * by intros m i; rewrite !lookup_unit ra_unit_idempotent.
+  * intros n m Hm i; apply cmra_validN_S, Hm.
+  * by intros m1 m2 m3 i; rewrite !lookup_op associative.
+  * by intros m1 m2 i; rewrite !lookup_op commutative.
+  * by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l.
+  * by intros m i; rewrite !lookup_unit cmra_unit_idempotent.
   * intros n x y; rewrite !map_includedN_spec; intros Hm i.
-    by rewrite !lookup_unit; apply cmra_unit_preserving.
-  * intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i).
+    by rewrite !lookup_unit; apply cmra_unit_preservingN.
+  * intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
-  * intros x y n; rewrite map_includedN_spec; intros ? i.
+  * intros x y n; rewrite map_includedN_spec=> ? i.
     by rewrite lookup_op lookup_minus cmra_op_minus.
 Qed.
-Global Instance map_ra_empty : RAIdentity (gmap K A).
-Proof.
-  split.
-  * by intros ?; rewrite lookup_empty.
-  * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
-Qed.
 Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
 Proof.
   intros n m m1 m2 Hm Hm12.
@@ -153,6 +144,14 @@ Proof.
 Qed.
 Canonical Structure mapRA : cmraT :=
   CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin.
+Global Instance map_cmra_identity : CMRAIdentity mapRA.
+Proof.
+  split.
+  * by intros ? n; rewrite lookup_empty.
+  * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
+  * apply map_empty_timeless.
+Qed.
+
 End cmra.
 Arguments mapRA _ {_ _} _.
 
@@ -180,7 +179,7 @@ Proof.
   split.
   * move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hm.
     destruct (m' !! i) as [y|];
-      [exists (x â‹… y)|exists x]; eauto using @ra_included_l.
+      [exists (x â‹… y)|exists x]; eauto using cmra_included_l.
   * intros (y&Hi&?); rewrite map_includedN_spec=>j.
     destruct (decide (i = j)); simplify_map_equality.
     + by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN.
diff --git a/modures/logic.v b/modures/logic.v
index 1a8a4c12e515f731d0b77e2917d802b28cf50938..f14b3da45bcddbe047795b83f633f7ae954c549f 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -55,14 +55,10 @@ Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed.
 
 Lemma uPred_holds_ne {M} (P1 P2 : uPred M) n x :
   P1 ={n}= P2 → ✓{n} x → P1 n x → P2 n x.
-Proof.
-  intros HP ?. apply HP; by auto.
-Qed.
+Proof. intros HP ?; apply HP; auto. Qed.
 Lemma uPred_weaken' {M} (P : uPred M) x1 x2 n1 n2 :
   x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → P n1 x1 → P n2 x2.
-Proof.
-  intros; eauto using uPred_weaken.
-Qed.
+Proof. eauto using uPred_weaken. Qed.
 
 (** functor *)
 Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
@@ -156,11 +152,11 @@ Next Obligation. by intros M P Q x; exists x, x. Qed.
 Next Obligation.
   intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
   assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
-  { destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using @ra_included_l.
+  { destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using cmra_included_l.
     apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
   clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
-  * apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
-  * apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
+  * apply uPred_weaken with x1 n1; eauto using cmra_validN_op_l.
+  * apply uPred_weaken with x2 n1; eauto using cmra_validN_op_r.
 Qed.
 
 Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
@@ -175,7 +171,7 @@ Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
 Next Obligation.
   intros M P Q x1 x2 n1 n2 HPQ ??? x3 n3 ???; simpl in *.
   apply uPred_weaken with (x1 â‹… x3) n3;
-    eauto using cmra_valid_included, @ra_preserving_r.
+    eauto using cmra_validN_included, cmra_preserving_r.
 Qed.
 
 Program Definition uPred_later {M} (P : uPred M) : uPred M :=
@@ -183,7 +179,7 @@ Program Definition uPred_later {M} (P : uPred M) : uPred M :=
 Next Obligation. intros M P ?? [|n]; eauto using uPred_ne,(dist_le (A:=M)). Qed.
 Next Obligation. done. Qed.
 Next Obligation.
-  intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken, cmra_valid_S.
+  intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken, cmra_validN_S.
 Qed.
 Program Definition uPred_always {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (unit x) |}.
@@ -191,7 +187,7 @@ Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
 Next Obligation. by intros; simpl. Qed.
 Next Obligation.
   intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
-    eauto using @ra_unit_preserving, cmra_unit_valid.
+    eauto using cmra_unit_preserving, cmra_unit_validN.
 Qed.
 
 Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
@@ -204,7 +200,7 @@ Next Obligation.
 Qed.
 Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
   {| uPred_holds n x := ✓{n} a |}.
-Solve Obligations with naive_solver eauto 2 using cmra_valid_le, cmra_valid_0.
+Solve Obligations with naive_solver eauto 2 using cmra_validN_le, cmra_validN_0.
 
 Delimit Scope uPred_scope with I.
 Bind Scope uPred_scope with uPred.
@@ -303,7 +299,7 @@ Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
 Proof.
   intros P P' HP Q Q' HQ x n' ??; split; intros (x1&x2&?&?&?); cofe_subst x;
     exists x1, x2; split_ands; try (apply HP || apply HQ);
-    eauto using cmra_valid_op_l, cmra_valid_op_r.
+    eauto using cmra_validN_op_l, cmra_validN_op_r.
 Qed.
 Global Instance sep_proper :
   Proper ((≡) ==> (≡) ==> (≡)) (@uPred_sep M) := ne_proper_2 _.
@@ -311,7 +307,7 @@ Global Instance wand_ne n :
   Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
 Proof.
   intros P P' HP Q Q' HQ x n' ??; split; intros HPQ x' n'' ???;
-    apply HQ, HPQ, HP; eauto using cmra_valid_op_r.
+    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
 Qed.
 Global Instance wand_proper :
   Proper ((≡) ==> (≡) ==> (≡)) (@uPred_wand M) := ne_proper_2 _.
@@ -343,12 +339,12 @@ Qed.
 Global Instance later_contractive : Contractive (@uPred_later M).
 Proof.
   intros n P Q HPQ x [|n'] ??; simpl; [done|].
-  apply HPQ; eauto using cmra_valid_S.
+  apply HPQ; eauto using cmra_validN_S.
 Qed.
 Global Instance later_proper :
   Proper ((≡) ==> (≡)) (@uPred_later M) := ne_proper _.
 Global Instance always_ne n: Proper (dist n ==> dist n) (@uPred_always M).
-Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_valid. Qed.
+Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_validN. Qed.
 Global Instance always_proper :
   Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _.
 Global Instance own_ne n : Proper (dist n ==> dist n) (@uPred_own M).
@@ -408,11 +404,11 @@ Lemma eq_rewrite {A : cofeT} P (Q : A → uPred M)
 Proof.
   intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
 Qed.
-Lemma eq_equiv `{Empty M, !RAIdentity M} {A : cofeT} (a b : A) :
+Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
   True ⊑ (a ≡ b) → a ≡ b.
 Proof.
   intros Hab; apply equiv_dist; intros n; apply Hab with ∅.
-  * apply cmra_valid_validN, ra_empty_valid.
+  * apply cmra_valid_validN, cmra_empty_valid.
   * by destruct n.
 Qed.
 Lemma iff_equiv P Q : True ⊑ (P ↔ Q) → P ≡ Q.
@@ -445,27 +441,14 @@ Proof. intros; apply impl_elim with Q; auto. Qed.
 Lemma impl_elim_r' P Q R : Q ⊑ (P → R) → (P ∧ Q) ⊑ R.
 Proof. intros; apply impl_elim with P; auto. Qed.
 Lemma impl_entails P Q : True ⊑ (P → Q) → P ⊑ Q.
-Proof.
-  intros H; eapply impl_elim; last reflexivity. rewrite -H.
-  by apply True_intro.
-Qed.
+Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
 Lemma entails_impl P Q : (P ⊑ Q) → True ⊑ (P → Q).
-Proof.
-  intros H; apply impl_intro_l. by rewrite -H and_elim_l.
-Qed.
+Proof. auto using impl_intro_l. Qed.
 
-Lemma const_intro_l φ Q R :
-  φ → (■φ ∧ Q) ⊑ R → Q ⊑ R.
-Proof.
-  intros ? <-. apply and_intro; last done.
-  by apply const_intro.
-Qed.
+Lemma const_intro_l φ Q R : φ → (■φ ∧ Q) ⊑ R → Q ⊑ R.
+Proof. intros ? <-; auto using const_intro. Qed.
 Lemma const_intro_r φ Q R : φ → (Q ∧ ■φ) ⊑ R → Q ⊑ R.
-Proof.
-  (* FIXME RJ: Why does this not work? rewrite (commutative uPred_and Q (■φ)%I). *)
-  intros ? <-. apply and_intro; first done.
-  by apply const_intro.
-Qed.
+Proof. intros ? <-; auto using const_intro. Qed.
 Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■ φ ∧ Q) ⊑ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
 Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■ φ) ⊑ R.
@@ -560,13 +543,13 @@ Proof. by rewrite -!(commutative _ R) and_or_l. Qed.
 Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
 Proof.
   intros HQ HQ' x n' ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
-    eauto 7 using cmra_valid_op_l, cmra_valid_op_r.
+    eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
 Qed.
 Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
 Proof.
   intros P x n Hvalid; split.
-  * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, @ra_included_r.
-  * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite ra_unit_l].
+  * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
+  * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite cmra_unit_l].
 Qed. 
 Global Instance sep_commutative : Commutative (≡) (@uPred_sep M).
 Proof.
@@ -587,7 +570,7 @@ Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
 Proof.
   intros HPQR x n ?? x' n' ???; apply HPQR; auto.
   exists x, x'; split_ands; auto.
-  eapply uPred_weaken with x n; eauto using cmra_valid_op_l.
+  eapply uPred_weaken with x n; eauto using cmra_validN_op_l.
 Qed.
 Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q.
 Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
@@ -617,15 +600,9 @@ Lemma sep_elim_r' P Q R : Q ⊑ R → (P ★ Q) ⊑ R.
 Proof. intros ->; apply sep_elim_r. Qed.
 Hint Resolve sep_elim_l' sep_elim_r'.
 Lemma sep_intro_True_l P Q R : True ⊑ P → R ⊑ Q → R ⊑ (P ★ Q).
-Proof.
-  intros HP HQ. etransitivity; last (eapply sep_mono; eassumption).
-  by rewrite left_id.
-Qed.
+Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
 Lemma sep_intro_True_r P Q R : R ⊑ P → True ⊑ Q → R ⊑ (P ★ Q).
-Proof.
-  intros HP HQ. etransitivity; last (eapply sep_mono; eassumption).
-  by rewrite right_id.
-Qed.
+Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
 Lemma wand_intro_l P Q R : (Q ★ P) ⊑ R → P ⊑ (Q -★ R).
 Proof. rewrite (commutative _); apply wand_intro_r. Qed.
 Lemma wand_elim_r P Q : (P ★ (P -★ Q)) ⊑ Q.
@@ -666,16 +643,16 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 
 (* Later *)
 Lemma later_mono P Q : P ⊑ Q → ▷ P ⊑ ▷ Q.
-Proof. intros HP x [|n] ??; [done|apply HP; eauto using cmra_valid_S]. Qed.
+Proof. intros HP x [|n] ??; [done|apply HP; eauto using cmra_validN_S]. Qed.
 Lemma later_intro P : P ⊑ ▷ P.
 Proof.
   intros x [|n] ??; simpl in *; [done|].
-  apply uPred_weaken with x (S n); eauto using cmra_valid_S.
+  apply uPred_weaken with x (S n); eauto using cmra_validN_S.
 Qed.
 Lemma löb P : (▷ P → P) ⊑ P.
 Proof.
   intros x n ? HP; induction n as [|n IH]; [by apply HP|].
-  apply HP, IH, uPred_weaken with x (S n); eauto using cmra_valid_S.
+  apply HP, IH, uPred_weaken with x (S n); eauto using cmra_validN_S.
 Qed.
 Lemma later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
 Proof. by intros x [|n]; split. Qed.
@@ -693,7 +670,7 @@ Proof.
   intros x n ?; split.
   * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
     destruct (cmra_extend_op n x x1 x2)
-      as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_valid_S; simpl in *.
+      as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
     exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
   * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
     exists x1, x2; eauto using dist_S.
@@ -724,12 +701,12 @@ Proof. done. Qed.
 Lemma always_elim P : □ P ⊑ P.
 Proof.
   intros x n ??; apply uPred_weaken with (unit x) n;
-    eauto using @ra_included_unit.
+    eauto using cmra_included_unit.
 Qed.
 Lemma always_intro P Q : □ P ⊑ Q → □ P ⊑ □ Q.
 Proof.
-  intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_valid.
-  by rewrite ra_unit_idempotent.
+  intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
+  by rewrite cmra_unit_idempotent.
 Qed.
 Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
 Proof. done. Qed.
@@ -741,12 +718,12 @@ Lemma always_exist {A} (P : A → uPred M) : (□ ∃ a, P a)%I ≡ (∃ a, □
 Proof. done. Qed.
 Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊑ □ (P ★ Q).
 Proof.
-  intros x n ? [??]; exists (unit x), (unit x); rewrite ra_unit_unit; auto.
+  intros x n ? [??]; exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
 Qed.
 Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊑ (□ P ★ Q).
 Proof.
   intros x n ? [??]; exists (unit x), x; simpl in *.
-  by rewrite ra_unit_l ra_unit_idempotent.
+  by rewrite cmra_unit_l cmra_unit_idempotent.
 Qed.
 Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
 Proof. done. Qed.
@@ -787,26 +764,10 @@ Proof.
   apply always_intro, impl_intro_r.
   by rewrite always_and_sep_l always_elim wand_elim_l.
 Qed.
-Lemma always_impl_l P Q : (P → □ Q) ⊑ (P → □ Q ★ P).
-Proof.
-  rewrite -always_and_sep_l. apply impl_intro_l, and_intro.
-  - by rewrite impl_elim_r.
-  - by rewrite and_elim_l.
-Qed.
-Lemma always_impl_r P Q : (P → □ Q) ⊑ (P → P ★ □ Q).
-Proof.
-  by rewrite commutative always_impl_l.
-Qed.
 Lemma always_entails_l P Q : (P ⊑ □ Q) → P ⊑ (□ Q ★ P).
-Proof.
-  intros H. apply impl_entails. rewrite -always_impl_l.
-  by apply entails_impl.
-Qed.
+Proof. intros; rewrite -always_and_sep_l; auto. Qed.
 Lemma always_entails_r P Q : (P ⊑ □ Q) → P ⊑ (P ★ □ Q).
-Proof.
-  intros H. apply impl_entails. rewrite -always_impl_r.
-  by apply entails_impl.
-Qed.
+Proof. intros; rewrite -always_and_sep_r; auto. Qed.
 
 (* Own *)
 Lemma own_op (a1 a2 : M) :
@@ -814,7 +775,7 @@ Lemma own_op (a1 a2 : M) :
 Proof.
   intros x n ?; split.
   * intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (associative op)|].
-    split. by exists (unit a1); rewrite ra_unit_r. by exists z.
+    split. by exists (unit a1); rewrite cmra_unit_r. by exists z.
   * intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
     by rewrite (associative op _ z1) -(commutative op z1) (associative op z1)
       -(associative op _ a2) (commutative op z1) -Hy1 -Hy2.
@@ -822,20 +783,20 @@ Qed.
 Lemma always_own_unit (a : M) : (□ uPred_own (unit a))%I ≡ uPred_own (unit a).
 Proof.
   intros x n; split; [by apply always_elim|intros [a' Hx]]; simpl.
-  rewrite -(ra_unit_idempotent a) Hx.
-  apply cmra_unit_preserving, cmra_included_l.
+  rewrite -(cmra_unit_idempotent a) Hx.
+  apply cmra_unit_preservingN, cmra_includedN_l.
 Qed.
 Lemma always_own (a : M) : unit a ≡ a → (□ uPred_own a)%I ≡ uPred_own a.
 Proof. by intros <-; rewrite always_own_unit. Qed.
-Lemma own_empty `{Empty M, !RAIdentity M} : True ⊑ uPred_own ∅.
+Lemma own_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_own ∅.
 Proof. intros x [|n] ??; [done|]. by  exists x; rewrite (left_id _ _). Qed.
 Lemma own_valid (a : M) : uPred_own a ⊑ (✓ a).
-Proof. move => x n Hv [a' ?]; cofe_subst; eauto using cmra_valid_op_l. Qed.
+Proof. move => x n Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
 Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊑ (✓ a).
 Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
 Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{1} a → (✓ a) ⊑ False.
 Proof.
-  intros Ha x [|n] ??; [|apply Ha, cmra_valid_le with (S n)]; auto with lia.
+  intros Ha x [|n] ??; [|apply Ha, cmra_validN_le with (S n)]; auto with lia.
 Qed.
 Lemma valid_mono {A B : cmraT} (a : A) (b : B) :
   (∀ n, ✓{n} a → ✓{n} b) → (✓ a) ⊑ (✓ b).
@@ -886,9 +847,9 @@ Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 1 x → P n x.
 Proof.
   split.
   * intros HP x n ??; induction n as [|[|n]]; auto.
-    by destruct (HP x (S (S n))); auto using cmra_valid_S.
+    by destruct (HP x (S (S n))); auto using cmra_validN_S.
   * move=> HP x [|[|n]] /=; auto; left.
-    apply HP, uPred_weaken with x (S n); eauto using cmra_valid_le.
+    apply HP, uPred_weaken with x (S n); eauto using cmra_validN_le.
 Qed.
 Global Instance const_timeless φ : TimelessP (■ φ : uPred M)%I.
 Proof. by apply timelessP_spec=> x [|n]. Qed.
@@ -901,7 +862,7 @@ Qed.
 Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
 Proof.
   rewrite !timelessP_spec=> HP x [|n] ? HPQ x' [|n'] ????; auto.
-  apply HP, HPQ, uPred_weaken with x' (S n'); eauto using cmra_valid_le.
+  apply HP, HPQ, uPred_weaken with x' (S n'); eauto using cmra_validN_le.
 Qed.
 Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q).
 Proof.
@@ -914,7 +875,7 @@ Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
 Proof.
   rewrite !timelessP_spec=> HP x [|n] ? HPQ x' [|n'] ???; auto.
   apply HP, HPQ, uPred_weaken with x' (S n');
-    eauto 3 using cmra_valid_le, cmra_valid_op_r.
+    eauto 3 using cmra_validN_le, cmra_validN_op_r.
 Qed.
 Global Instance forall_timeless {A} (P : A → uPred M) :
   (∀ x, TimelessP (P x)) → TimelessP (∀ x, P x).
@@ -933,10 +894,10 @@ Qed.
 Global Instance eq_timeless {A : cofeT} (a b : A) :
   Timeless a → TimelessP (a ≡ b : uPred M)%I.
 Proof. by intro; apply timelessP_spec=> x n ??; apply equiv_dist, timeless. Qed.
-Global Instance own_timeless (a : M): Timeless a → TimelessP (uPred_own a).
+Global Instance own_timeless (a : M) : Timeless a → TimelessP (uPred_own a).
 Proof.
-  intro; apply timelessP_spec=> x [|n] ?? //; apply cmra_included_includedN,
-    cmra_timeless_included_l; eauto using cmra_valid_le.
+  intros ?; apply timelessP_spec=> x [|n] ?? //; apply cmra_included_includedN,
+    cmra_timeless_included_l; eauto using cmra_validN_le.
 Qed.
 
 (* Always stable *)
@@ -979,10 +940,6 @@ Lemma always_and_sep_r' P Q `{!AlwaysStable Q} : (P ∧ Q)%I ≡ (P ★ Q)%I.
 Proof. by rewrite -(always_always Q) always_and_sep_r. Qed.
 Lemma always_sep_dup' P `{!AlwaysStable P} : P ≡ (P ★ P)%I.
 Proof. by rewrite -(always_always P) -always_sep_dup. Qed.
-Lemma always_impl_l' P Q `{!AlwaysStable Q} : (P → Q) ⊑ (P → Q ★ P).
-Proof. by rewrite -(always_always Q) always_impl_l. Qed.
-Lemma always_impl_r' P Q `{!AlwaysStable Q} : (P → Q) ⊑ (P → P ★ Q).
-Proof. by rewrite -(always_always Q) always_impl_r. Qed.
 Lemma always_entails_l' P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (Q ★ P).
 Proof. by rewrite -(always_always Q); apply always_entails_l. Qed.
 Lemma always_entails_r' P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (P ★ Q).
diff --git a/modures/option.v b/modures/option.v
index 256331bfad728d80eec71313f8d0e6743be0a142..0b32c1180a2c088c1812e631aafd9d933b401dca 100644
--- a/modures/option.v
+++ b/modures/option.v
@@ -66,25 +66,12 @@ Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
 Section cmra.
 Context {A : cmraT}.
 
-Instance option_valid : Valid (option A) := λ mx,
-  match mx with Some x => ✓ x | None => True end.
 Instance option_validN : ValidN (option A) := λ n mx,
   match mx with Some x => ✓{n} x | None => True end.
 Instance option_unit : Unit (option A) := fmap unit.
 Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
 Instance option_minus : Minus (option A) :=
   difference_with (λ x y, Some (x ⩪ y)).
-Lemma option_included mx my :
-  mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y.
-Proof.
-  split.
-  * intros [mz Hmz]; destruct mx as [x|]; [right|by left].
-    destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
-    destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
-      setoid_subst; eauto using ra_included_l.
-  * intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
-    by exists (Some z); constructor.
-Qed.
 Lemma option_includedN n (mx my : option A) :
   mx ≼{n} my ↔ n = 0 ∨ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
 Proof.
@@ -93,7 +80,7 @@ Proof.
     destruct mx as [x|]; [right|by left].
     destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
     destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
-      cofe_subst; eauto using @cmra_included_l.
+      cofe_subst; eauto using cmra_includedN_l.
   * intros [->|[->|(x&y&->&->&z&Hz)]];
       try (by exists my; destruct my; constructor).
     by exists (Some z); constructor.
@@ -110,22 +97,20 @@ Proof.
       repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
   * by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _).
   * destruct 1 as [[?|] [?|]| |]; unfold validN, option_validN; simpl;
-     intros ?; auto using cmra_valid_0;
+     intros ?; auto using cmra_validN_0;
      eapply (_ : Proper (dist _ ==> impl) (✓{_})); eauto.
   * by destruct 1; inversion_clear 1; constructor;
       repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
-  * intros [x|]; unfold validN, option_validN; auto using cmra_valid_0.
-  * intros n [x|]; unfold validN, option_validN; eauto using @cmra_valid_S.
-  * by intros [x|]; unfold valid, validN, option_validN, option_valid;
-      eauto using cmra_valid_validN.
-  * intros [x|] [y|] [z|]; constructor; rewrite ?(associative _); auto.
-  * intros [x|] [y|]; constructor; rewrite 1?(commutative _); auto.
-  * by intros [x|]; constructor; rewrite ra_unit_l.
-  * by intros [x|]; constructor; rewrite ra_unit_idempotent.
+  * intros [x|]; unfold validN, option_validN; auto using cmra_validN_0.
+  * intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
+  * intros [x|] [y|] [z|]; constructor; rewrite ?associative; auto.
+  * intros [x|] [y|]; constructor; rewrite 1?commutative; auto.
+  * by intros [x|]; constructor; rewrite cmra_unit_l.
+  * by intros [x|]; constructor; rewrite cmra_unit_idempotent.
   * intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto.
-    do 2 right; exists (unit x), (unit y); eauto using @cmra_unit_preserving.
-  * intros n [x|] [y|]; unfold validN, option_validN; simpl;
-      eauto using @cmra_valid_op_l.
+    do 2 right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
+  * intros n [x|] [y|]; rewrite /validN /option_validN /=;
+      eauto using cmra_validN_op_l.
   * intros n mx my; rewrite option_includedN.
     intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|].
     by constructor; apply cmra_op_minus.
diff --git a/modures/ra.v b/modures/ra.v
deleted file mode 100644
index 4401556a103147cac4987d9922a35fda7972e785..0000000000000000000000000000000000000000
--- a/modures/ra.v
+++ /dev/null
@@ -1,258 +0,0 @@
-Require Export prelude.collections prelude.relations prelude.fin_maps.
-Require Export modures.base.
-
-Class Valid (A : Type) := valid : A → Prop.
-Instance: Params (@valid) 2.
-Notation "✓" := valid (at level 1).
-
-Class Unit (A : Type) := unit : A → A.
-Instance: Params (@unit) 2.
-
-Class Op (A : Type) := op : A → A → A.
-Instance: Params (@op) 2.
-Infix "â‹…" := op (at level 50, left associativity) : C_scope.
-Notation "(â‹…)" := op (only parsing) : C_scope.
-
-Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
-Infix "≼" := included (at level 70) : C_scope.
-Notation "(≼)" := included (only parsing) : C_scope.
-Hint Extern 0 (?x ≼ ?y) => reflexivity.
-Instance: Params (@included) 3.
-
-Class Minus (A : Type) := minus : A → A → A.
-Instance: Params (@minus) 2.
-Infix "⩪" := minus (at level 40) : C_scope.
-
-Class RA A `{Equiv A, Valid A, Unit A, Op A, Minus A} : Prop := {
-  (* setoids *)
-  ra_equivalence :> Equivalence ((≡) : relation A);
-  ra_op_proper x :> Proper ((≡) ==> (≡)) (op x);
-  ra_unit_proper :> Proper ((≡) ==> (≡)) unit;
-  ra_valid_proper :> Proper ((≡) ==> impl) ✓;
-  ra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus;
-  (* monoid *)
-  ra_associative :> Associative (≡) (⋅);
-  ra_commutative :> Commutative (≡) (⋅);
-  ra_unit_l x : unit x ⋅ x ≡ x;
-  ra_unit_idempotent x : unit (unit x) ≡ unit x;
-  ra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
-  ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x;
-  ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
-}.
-Class RAIdentity A `{Equiv A, Valid A, Op A, Empty A} : Prop := {
-  ra_empty_valid : ✓ ∅;
-  ra_empty_l :> LeftId (≡) ∅ (⋅)
-}.
-
-Class RAMonotone
-    `{Equiv A, Op A, Valid A, Equiv B, Op B, Valid B} (f : A → B) := {
-  included_preserving x y : x ≼ y → f x ≼ f y;
-  valid_preserving x : ✓ x → ✓ (f x)
-}.
-
-(** Big ops *)
-Fixpoint big_op `{Op A, Empty A} (xs : list A) : A :=
-  match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end.
-Arguments big_op _ _ _ !_ /.
-Instance: Params (@big_op) 3.
-
-Definition big_opM `{FinMapToList K A M, Op A, Empty A} (m : M) : A :=
-  big_op (snd <$> map_to_list m).
-Instance: Params (@big_opM) 6.
-
-(** Updates *)
-Definition ra_update_set `{Op A, Valid A} (x : A) (P : A → Prop) :=
-  ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z).
-Instance: Params (@ra_update_set) 3.
-Infix "⇝:" := ra_update_set (at level 70).
-Definition ra_update `{Op A, Valid A} (x y : A) := ∀ z,
-  ✓ (x ⋅ z) → ✓ (y ⋅ z).
-Infix "⇝" := ra_update (at level 70).
-Instance: Params (@ra_update) 3.
-
-(** Properties **)
-Section ra.
-Context `{RA A}.
-Implicit Types x y z : A.
-Implicit Types xs ys zs : list A.
-
-Global Instance ra_valid_proper' : Proper ((≡) ==> iff) ✓.
-Proof. by intros ???; split; apply ra_valid_proper. Qed.
-Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (⋅).
-Proof.
-  intros x1 x2 Hx y1 y2 Hy.
-  by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
-Qed.
-Lemma ra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y.
-Proof. rewrite (commutative _ x); apply ra_valid_op_l. Qed.
-
-(** ** Units *)
-Lemma ra_unit_r x : x ⋅ unit x ≡ x.
-Proof. by rewrite (commutative _ x) ra_unit_l. Qed.
-Lemma ra_unit_unit x : unit x ⋅ unit x ≡ unit x.
-Proof. by rewrite -{2}(ra_unit_idempotent x) ra_unit_r. Qed.
-
-(** ** Order *)
-Instance ra_included_proper' : Proper ((≡) ==> (≡) ==> impl) (≼).
-Proof. intros x1 x2 Hx y1 y2 Hy [z Hz]; exists z. by rewrite -Hy Hz Hx. Qed.
-Global Instance ra_included_proper : Proper ((≡) ==> (≡) ==> iff) (≼).
-Proof. by split; apply ra_included_proper'. Qed.
-Lemma ra_included_l x y : x ≼ x ⋅ y.
-Proof. by exists y. Qed.
-Lemma ra_included_r x y : y ≼ x ⋅ y.
-Proof. rewrite (commutative op); apply ra_included_l. Qed.
-Global Instance: PreOrder included.
-Proof.
-  split; first by intros x; exists (unit x); rewrite ra_unit_r.
-  intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
-  by rewrite (associative _) -Hy -Hz.
-Qed.
-Lemma ra_included_unit x : unit x ≼ x.
-Proof. by exists x; rewrite ra_unit_l. Qed.
-Lemma ra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
-Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative (â‹…)). Qed.
-Lemma ra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
-Proof. by intros; rewrite -!(commutative _ z); apply ra_preserving_l. Qed.
-
-(** ** RAs with empty element *)
-Context `{Empty A, !RAIdentity A}.
-
-Global Instance ra_empty_r : RightId (≡) ∅ (⋅).
-Proof. by intros x; rewrite (commutative op) (left_id _ _). Qed.
-Lemma ra_unit_empty : unit ∅ ≡ ∅.
-Proof. by rewrite -{2}(ra_unit_l ∅) (right_id _ _). Qed.
-Lemma ra_empty_least x : ∅ ≼ x.
-Proof. by exists x; rewrite (left_id _ _). Qed.
-
-(** * Big ops *)
-Lemma big_op_nil : big_op (@nil A) = ∅.
-Proof. done. Qed.
-Lemma big_op_cons x xs : big_op (x :: xs) = x â‹… big_op xs.
-Proof. done. Qed.
-Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
-Proof.
-  induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
-  * by rewrite IH.
-  * by rewrite !(associative _) (commutative _ x).
-  * by transitivity (big_op xs2).
-Qed.
-Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
-Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
-Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
-Proof.
-  induction xs as [|x xs IH]; simpl; first by rewrite ?(left_id _ _).
-  by rewrite IH (associative _).
-Qed.
-Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys.
-Proof.
-  induction 1 as [|x xs ys|x y xs|x xs ys|xs ys zs]; rewrite //=.
-  * by apply ra_preserving_l.
-  * by rewrite !(associative _) (commutative _ y); apply ra_preserving_r.
-  * by transitivity (big_op ys); [|apply ra_included_r].
-  * by transitivity (big_op ys).
-Qed.
-Lemma big_op_delete xs i x :
-  xs !! i = Some x → x ⋅ big_op (delete i xs) ≡ big_op xs.
-Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.
-
-Context `{FinMap K M}.
-Lemma big_opM_empty : big_opM (∅ : M A) ≡ ∅.
-Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
-Lemma big_opM_insert (m : M A) i x :
-  m !! i = None → big_opM (<[i:=x]> m) ≡ x ⋅ big_opM m.
-Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
-Lemma big_opM_delete (m : M A) i x :
-  m !! i = Some x → x ⋅ big_opM (delete i m) ≡ big_opM m.
-Proof.
-  intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete.
-Qed.
-Lemma big_opM_singleton i x : big_opM ({[i ↦ x]} : M A) ≡ x.
-Proof.
-  rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
-  by rewrite big_opM_empty (right_id _ _).
-Qed.
-Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : M A → _).
-Proof.
-  intros m1; induction m1 as [|i x m1 ? IH] using map_ind.
-  { by intros m2; rewrite (symmetry_iff (≡)) map_equiv_empty; intros ->. }
-  intros m2 Hm2; rewrite big_opM_insert //.
-  rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
-  destruct (map_equiv_lookup (<[i:=x]> m1) m2 i x)
-    as (y&?&Hxy); auto using lookup_insert.
-  rewrite Hxy -big_opM_insert; last auto using lookup_delete.
-  by rewrite insert_delete.
-Qed.
-End ra.
-
-(* Simple solver for inclusion by reflection *)
-Module ra_reflection. Section ra_reflection.
-  Context `{RA A, Empty A, !RAIdentity A}.
-
-  Inductive expr :=
-    | EVar : nat → expr
-    | EEmpty : expr
-    | EOp : expr → expr → expr.
-  Fixpoint eval (Σ : list A) (e : expr) : A :=
-    match e with
-    | EVar n => from_option ∅ (Σ !! n)
-    | EEmpty => ∅
-    | EOp e1 e2 => eval Σ e1 ⋅ eval Σ e2
-    end.
-  Fixpoint flatten (e : expr) : list nat :=
-    match e with
-    | EVar n => [n]
-    | EEmpty => []
-    | EOp e1 e2 => flatten e1 ++ flatten e2
-    end.
-  Lemma eval_flatten Σ e :
-    eval Σ e ≡ big_op ((λ n, from_option ∅ (Σ !! n)) <$> flatten e).
-  Proof.
-    by induction e as [| |e1 IH1 e2 IH2];
-      rewrite /= ?(right_id _ _) ?fmap_app ?big_op_app ?IH1 ?IH2.
-  Qed.
-  Lemma flatten_correct Σ e1 e2 :
-    flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.
-  Proof.
-    by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He.
-  Qed.
-
-  Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
-  Global Instance quote_empty: Quote E1 E1 ∅ EEmpty.
-  Global Instance quote_var Σ1 Σ2 e i:
-    rlist.QuoteLookup Σ1 Σ2 e i → Quote Σ1 Σ2 e (EVar i) | 1000.
-  Global Instance quote_app Σ1 Σ2 Σ3 x1 x2 e1 e2 :
-    Quote Σ1 Σ2 x1 e1 → Quote Σ2 Σ3 x2 e2 → Quote Σ1 Σ3 (x1 ⋅ x2) (EOp e1 e2).
-  End ra_reflection.
-
-  Ltac quote :=
-    match goal with
-    | |- @included _ _ _ ?x ?y =>
-      lazymatch type of (_ : Quote [] _ x _) with Quote _ ?Σ2 _ ?e1 =>
-      lazymatch type of (_ : Quote Σ2 _ y _) with Quote _ ?Σ3 _ ?e2 =>
-        change (eval Σ3 e1 ≼ eval Σ3 e2)
-      end end
-    end.
-End ra_reflection.
-
-Ltac solve_included :=
-  ra_reflection.quote;
-  apply ra_reflection.flatten_correct, (bool_decide_unpack _);
-  vm_compute; apply I.
-
-(** An RA for the unit type *)
-Instance unit_valid : Valid () := λ x, True.
-Instance unit_unit : Unit () := λ x, x.
-Instance unit_op : Op () := λ x y, tt.
-Instance unit_minus : Minus () := λ x y, tt.
-
-Instance unit_ra : RA ().
-Proof.
-  split; done.
-Qed.
-
-
-Instance unit_empty : Empty () := tt.
-Instance unit_empty_ra : RAIdentity().
-Proof.
-  split; done.
-Qed.
diff --git a/modures/sts.v b/modures/sts.v
index e4977886b5b20def0d147d4f98ac58d79617a94d..4697c82c0e85895637d663873caa72d58626786d 100644
--- a/modures/sts.v
+++ b/modures/sts.v
@@ -1,21 +1,21 @@
-Require Export modures.ra.
+Require Export modures.cmra.
 Require Import prelude.sets modures.dra.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments unit _ _ !_ /.
 
-Module sts.
-Inductive t {A B} (R : relation A) (tok : A → set B) :=
-  | auth : A → set B → t R tok
-  | frag : set A → set B → t R tok.
+Inductive sts {A B} (R : relation A) (tok : A → set B) :=
+  | auth : A → set B → sts R tok
+  | frag : set A → set B → sts R tok.
 Arguments auth {_ _ _ _} _ _.
 Arguments frag {_ _ _ _} _ _.
 
+Module sts.
 Section sts_core.
 Context {A B : Type} (R : relation A) (tok : A → set B).
 Infix "≼" := dra_included.
 
-Inductive sts_equiv : Equiv (t R tok) :=
+Inductive sts_equiv : Equiv (sts R tok) :=
   | auth_equiv s T1 T2 : T1 ≡ T2 → auth s T1 ≡ auth s T2
   | frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
 Global Existing Instance sts_equiv.
@@ -36,28 +36,28 @@ Record closed (T : set B) (S : set A) : Prop := Closed {
 Lemma closed_steps S T s1 s2 :
   closed T S → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S.
 Proof. induction 3; eauto using closed_step. Qed.
-Global Instance sts_valid : Valid (t R tok) := λ x,
+Global Instance sts_valid : Valid (sts R tok) := λ x,
   match x with auth s T => tok s ∩ T ≡ ∅ | frag S' T => closed T S' end.
 Definition up (T : set B) (s : A) : set A := mkSet (rtc (frame_step T) s).
 Definition up_set (T : set B) (S : set A) : set A := S ≫= up T.
-Global Instance sts_unit : Unit (t R tok) := λ x,
+Global Instance sts_unit : Unit (sts R tok) := λ x,
   match x with
   | frag S' _ => frag (up_set ∅ S') ∅ | auth s _ => frag (up ∅ s) ∅
   end.
-Inductive sts_disjoint : Disjoint (t R tok) :=
+Inductive sts_disjoint : Disjoint (sts R tok) :=
   | frag_frag_disjoint S1 S2 T1 T2 :
      S1 ∩ S2 ≢ ∅ → T1 ∩ T2 ≡ ∅ → frag S1 T1 ⊥ frag S2 T2
   | auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ∩ T2 ≡ ∅ → auth s T1 ⊥ frag S T2
   | frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ∩ T2 ≡ ∅ → frag S T1 ⊥ auth s T2.
 Global Existing Instance sts_disjoint.
-Global Instance sts_op : Op (t R tok) := λ x1 x2,
+Global Instance sts_op : Op (sts R tok) := λ x1 x2,
   match x1, x2 with
   | frag S1 T1, frag S2 T2 => frag (S1 ∩ S2) (T1 ∪ T2)
   | auth s T1, frag _ T2 => auth s (T1 ∪ T2)
   | frag _ T1, auth s T2 => auth s (T1 ∪ T2)
   | auth s T1, auth _ T2 => auth s (T1 ∪ T2) (* never happens *)
   end.
-Global Instance sts_minus : Minus (t R tok) := λ x1 x2,
+Global Instance sts_minus : Minus (sts R tok) := λ x1 x2,
   match x1, x2 with
   | frag S1 T1, frag S2 T2 => frag (up_set (T1 ∖ T2) S1) (T1 ∖ T2)
   | auth s T1, frag _ T2 => auth s (T1 ∖ T2)
@@ -69,7 +69,7 @@ Hint Extern 10 (equiv (A:=set _) _ _) => solve_elem_of : sts.
 Hint Extern 10 (¬(equiv (A:=set _) _ _)) => solve_elem_of : sts.
 Hint Extern 10 (_ ∈ _) => solve_elem_of : sts.
 Hint Extern 10 (_ ⊆ _) => solve_elem_of : sts.
-Instance: Equivalence ((≡) : relation (t R tok)).
+Instance: Equivalence ((≡) : relation (sts R tok)).
 Proof.
   split.
   * by intros []; constructor.
@@ -135,7 +135,7 @@ Proof.
   unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
   induction Hstep; eauto using closed_step.
 Qed.
-Global Instance sts_dra : DRA (t R tok).
+Global Instance sts_dra : DRA (sts R tok).
 Proof.
   split.
   * apply _.
@@ -203,18 +203,12 @@ Qed.
 End sts_core.
 End sts.
 
-Section sts_ra.
+Section stsRA.
 Context {A B : Type} (R : relation A) (tok : A → set B).
 
-Definition sts := validity (✓ : sts.t R tok → Prop).
-Global Instance sts_equiv : Equiv sts := validity_equiv _.
-Global Instance sts_unit : Unit sts := validity_unit _.
-Global Instance sts_op : Op sts := validity_op _.
-Global Instance sts_minus : Minus sts := validity_minus _.
-Global Instance sts_ra : RA sts := validity_ra _.
-Definition sts_auth (s : A) (T : set B) : sts := to_validity (sts.auth s T).
-Definition sts_frag (S : set A) (T : set B) : sts := to_validity (sts.frag S T).
-Canonical Structure stsRA := validityRA (sts.t R tok).
+Canonical Structure stsRA := validityRA (sts R tok).
+Definition sts_auth (s : A) (T : set B) : stsRA := to_validity (auth s T).
+Definition sts_frag (S : set A) (T : set B) : stsRA := to_validity (frag S T).
 Lemma sts_update s1 s2 T1 T2 :
   sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ⇝ sts_auth s2 T2.
 Proof.
@@ -222,4 +216,4 @@ Proof.
   destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto.
   repeat (done || constructor).
 Qed.
-End sts_ra.
+End stsRA.
diff --git a/prelude/gmap.v b/prelude/gmap.v
index 917bfb29e0867c3debf6bcb3eb74f5985fb0339a..1c2cd5ec7865d8fb95e8b64bfb27d7443543f975 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -118,19 +118,16 @@ Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
 Instance gset_dom_spec `{Countable K} :
   FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
-(** * Fresh positive *)
-Definition Gfresh {A} (m : gmap positive A) : positive :=
-  Pfresh $ gmap_car m.
-Lemma Gfresh_fresh {A} (m : gmap positive A) : m !! Gfresh m = None.
-Proof. destruct m as [[]]. apply Pfresh_fresh; done. Qed. 
-
-Instance Gset_fresh : Fresh positive (gset positive) := λ X,
-  let (m) := X in Gfresh m.
-Instance Gset_fresh_spec : FreshSpec positive (gset positive).
+(** * Fresh elements *)
+(* This is pretty ad-hoc and just for the case of [gset positive]. We need a
+notion of countable non-finite types to generalize this. *)
+Instance gset_positive_fresh : Fresh positive (gset positive) := λ X,
+  let 'Mapset (GMap m _) := X in fresh (dom _ m).
+Instance gset_positive_fresh_spec : FreshSpec positive (gset positive).
 Proof.
   split.
   * apply _.
-  * intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
-  * unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
-    by rewrite Gfresh_fresh.
+  * by intros X Y; rewrite <-elem_of_equiv_L; intros ->.
+  * intros [[m Hm]]; unfold fresh; simpl.
+    by intros ?; apply (is_fresh (dom Pset m)), elem_of_dom_2 with ().
 Qed.