diff --git a/algebra/auth.v b/algebra/auth.v
index 2202a805d670912159d0371e9aba7b5ea617a019..5c72d423924f87502cea41bbf154363a4f33fa74 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -1,5 +1,5 @@
 Require Export algebra.excl.
-Require Import algebra.functor algebra.option.
+Require Import algebra.functor.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
@@ -148,7 +148,7 @@ Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b.
 Proof. by rewrite /op /auth_op /= left_id. Qed.
 
 (* FIXME tentative name. Or maybe remove this notion entirely. *)
-Definition auth_step a a' b b' :=
+Definition auth_step (a a' b b' : A) : Prop :=
   ∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b.
 
 Lemma auth_update a a' b b' :
@@ -160,27 +160,31 @@ Proof.
   { by rewrite Ha left_id associative. }
   split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
 Qed.
-Lemma auth_update_op_l a a' b :
-  ✓ (b ⋅ a) → ● a ⋅ ◯ a' ~~> ● (b ⋅ a) ⋅ ◯ (b ⋅ a').
+
+(* FIXME: are the following lemmas derivable from each other? *)
+Lemma auth_local_update_l f `{!LocalUpdate P f} a a' :
+  P a → ✓ (f a ⋅ a') →
+  ● (a ⋅ a') ⋅ ◯ a ~~> ● (f a ⋅ a') ⋅ ◯ f a.
+Proof.
+  intros; apply auth_update=>n af ? EQ; split; last done.
+  by rewrite -(local_updateN f) // EQ -(local_updateN f) // -EQ.
+Qed.
+
+Lemma auth_local_update f `{!LocalUpdate P f} a a' :
+  P a → ✓ (f a') →
+  ● a' ⋅ ◯ a ~~> ● f a' ⋅ ◯ f a.
 Proof.
-  intros; apply auth_update.
-  by intros n af ? Ha; split; [by rewrite Ha associative|].
+  intros; apply auth_update=>n af ? EQ; split; last done.
+  by rewrite EQ (local_updateN f) // -EQ.
 Qed.
+
+Lemma auth_update_op_l a a' b :
+  ✓ (b ⋅ a) → ● a ⋅ ◯ a' ~~> ● (b ⋅ a) ⋅ ◯ (b ⋅ a').
+Proof. by intros; apply (auth_local_update _). Qed.
 Lemma auth_update_op_r a a' b :
   ✓ (a ⋅ b) → ● a ⋅ ◯ a' ~~> ● (a ⋅ b) ⋅ ◯ (a' ⋅ b).
 Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed.
 
-Lemma auth_local_update (L : LocalUpdate A) `{!LocalUpdateSpec L} a a' b :
-  L a = Some b → ✓(b ⋅ a') →
-  ● (a ⋅ a') ⋅ ◯ a ~~> ● (b ⋅ a') ⋅ ◯ b.
-Proof.
-  intros Hlv Hv. apply auth_update=>n af Hab EQ.
-  split; last done.
-  apply (injective (R:=(≡)) Some).
-  rewrite !Some_op -Hlv.
-  rewrite -!local_update_spec //; eauto; last by rewrite -EQ; [].
-  by rewrite EQ.
-Qed.
 End cmra.
 
 Arguments authRA : clear implicits.
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 54c6c4a5d0dda2e70cf799d93672226d035d7e70..bfc450a974d62555665ff878dbd6389c9e2ad071 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -135,6 +135,13 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
   validN_preserving n x : ✓{n} x → ✓{n} (f x)
 }.
 
+(** * Local updates *)
+Class LocalUpdate {A : cmraT} (P : A → Prop) (f : A → A) := {
+  local_update_ne n :> Proper (dist n ==> dist n) f;
+  local_updateN n x y : P x → ✓{n} (x ⋅ y) → f (x ⋅ y) ≡{n}≡ f x ⋅ y
+}.
+Arguments local_updateN {_ _} _ {_} _ _ _ _ _.
+
 (** * Frame preserving updates *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
   ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
@@ -313,6 +320,18 @@ Section identity.
   Proof. by rewrite -{2}(cmra_unit_l ∅) right_id. Qed.
 End identity.
 
+(** ** Local updates *)
+Global Instance local_update_proper P (f : A → A) :
+  LocalUpdate P f → Proper ((≡) ==> (≡)) f.
+Proof. intros; apply (ne_proper _). Qed.
+
+Lemma local_update f `{!LocalUpdate P f} x y :
+  P x → ✓ (x ⋅ y) → f (x ⋅ y) ≡ f x ⋅ y.
+Proof. by rewrite equiv_dist=>?? n; apply (local_updateN f). Qed.
+
+Global Instance local_update_op x : LocalUpdate (λ _, True) (op x).
+Proof. split. apply _. by intros n y1 y2 _ _; rewrite associative. Qed.
+
 (** ** Updates *)
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
diff --git a/algebra/excl.v b/algebra/excl.v
index 7e8b226538feee294da327a2b14bb77674f67d82..db3d83f2fe7956c27334243a5cba4573cd962c14 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -1,5 +1,5 @@
 Require Export algebra.cmra.
-Require Import algebra.functor algebra.option.
+Require Import algebra.functor.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
@@ -138,23 +138,16 @@ Proof.
   by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
 Qed.
 
-(* Updates *)
+(** ** Local updates *)
+Global Instance excl_local_update b :
+  LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b).
+Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
+
+(** Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y.
 Proof. by destruct y; intros ? [?| |]. Qed.
 Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x ~~>: P.
 Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed.
-
-Definition excl_local_update_to (b : A) : LocalUpdate exclRA :=
-  λ a, if a is Excl _ then Some (Excl b) else None.
-Global Instance excl_local_update_to_spec b :
-  LocalUpdateSpec (excl_local_update_to b).
-Proof.
-  split.
-  - move=>? a a' EQ. destruct EQ; done.
-  - move=>a a' n [b' Hlv] Hv /=. destruct a; try discriminate Hlv; [].
-    destruct a'; try contradiction Hv; []. reflexivity.
-Qed.
-
 End excl.
 
 Arguments exclC : clear implicits.
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 9d5d841d8b4913b075c7af9f36ba90f5b1b8b256..c54e70b0d8a4715d93db217fff62fedc1f2e2e35 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -34,6 +34,12 @@ Global Instance lookup_ne n k :
 Proof. by intros m1 m2. Qed.
 Global Instance lookup_proper k :
   Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _.
+Global Instance alter_ne f k n :
+  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter f k).
+Proof.
+  intros ? m m' Hm k'.
+  by destruct (decide (k = k')); simplify_map_equality; rewrite (Hm k').
+Qed.
 Global Instance insert_ne i n :
   Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
 Proof.
@@ -280,47 +286,22 @@ Lemma map_updateP_alloc' m x :
 Proof. eauto using map_updateP_alloc. Qed.
 End freshness.
 
-Section local.
-Definition map_local_alloc i x : LocalUpdate (mapRA K A) :=
-  local_update_op {[ i ↦ x ]}.
-
 (* Deallocation is not a local update. The trouble is that if we own {[ i ↦ x ]},
    then the frame could always own "unit x", and prevent deallocation. *)
-
-Context (L : LocalUpdate A) `{!LocalUpdateSpec L}.
-Definition map_local_update i : LocalUpdate (mapRA K A) :=
-  λ m, x ← m !! i; y ← L x; Some (<[i:=y]>m).
-Global Instance map_local_update_spec i : LocalUpdateSpec (map_local_update i).
+(*
+Lemma option_fmap_op {B : cmraT} (f : A → B) (mx my : option A) : f <$> mx ⋅ my = (f <$> mx) ⋅ (f <$> my).
+Proof. destruct mx, my; simpl; try done.
+*)
+Global Instance map_alter_update `{!LocalUpdate P f} i :
+  LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ P x) (alter f i).
 Proof.
-  rewrite /map_local_update. split.
-  - (* FIXME Oh wow, this is harder than expected... *)
-    move=>n f g EQ. move:(EQ i).
-    case _:(f !! i)=>[fi|]; case _:(g !! i)=>[gi|]; move=>EQi;
-      inversion EQi; subst; simpl; last done.
-    assert (EQL : L fi ≡{n}≡ L gi) by (by apply local_update_ne). move: EQL.
-    case _:(L fi)=>[Lfi|] /=; case _:(L gi)=>[Lgi|]; move=>EQL;
-      inversion EQL; subst; simpl; last done.
-    apply Some_ne, insert_ne; done.
-  - move=>f g n [b Hlv] Hv. rewrite lookup_op. move:Hlv.
-    case EQf:(f !! i)=>[fi|]; simpl; last discriminate.
-    case EQL:(L fi)=>[Lfi|]; simpl; last discriminate.
-    case=>?. subst b.
-    case EQg:(g !! i)=>[gi|]; simpl.
-    + assert (L (fi ⋅ gi) ≡{n}≡ L fi ⋅ Some gi) as EQLi.
-      { apply local_update_spec; first by eauto.
-        move:(Hv i). rewrite lookup_op EQf EQg -Some_op. done. }
-      rewrite EQL -Some_op in EQLi.
-      destruct (L (fi â‹… gi)) as [Lfgi|]; inversion EQLi; subst; simpl.
-      rewrite -Some_op. apply Some_ne. move=>j. rewrite lookup_op.
-      destruct (decide (i = j)); simplify_map_equality; last by rewrite lookup_op.
-      rewrite EQg -Some_op. apply Some_ne. done.
-    + rewrite EQL /=.
-      rewrite -Some_op. apply Some_ne. move=>j. rewrite lookup_op.
-      destruct (decide (i = j)); simplify_map_equality; last by rewrite lookup_op.
-      by rewrite EQg.
+  split; first apply _.
+  intros n m1 m2 (x&Hix&?) Hm j; destruct (decide (i = j)) as [->|].
+  - rewrite lookup_alter !lookup_op lookup_alter Hix /=.
+    move: (Hm j); rewrite lookup_op Hix.
+    case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN f).
+  - by rewrite lookup_op !lookup_alter_ne // lookup_op.
 Qed.
-End local.
-
 End properties.
 
 (** Functor *)
@@ -358,4 +339,3 @@ Next Obligation.
   intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
   apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
 Qed.
-
diff --git a/algebra/option.v b/algebra/option.v
index c6584617dd56abd561b4716ca504909e296abd0d..d5bc0379e277e81345cf8f7238e827f71e1e0c0a 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -187,28 +187,3 @@ Next Obligation.
   intros Σ A B C f g x. rewrite /= -option_fmap_compose.
   apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
 Qed.
-
-(** * Local CMRA Updates *)
-(* FIXME: These need the CMRA structure on option, hence they are defined here. Or maybe moe option to cmra.v? *)
-(* TODO: Probably needs some more magic flags. What about notation? *)
-Section local_update.
-  Context {A : cmraT}.
-  (* Do we need more step-indexing here? *)
-  Definition LocalUpdate := A → option A.
-  Class LocalUpdateSpec (L : LocalUpdate) := {
-    local_update_ne n :> Proper ((dist n) ==> (dist n)) L;
-    local_update_spec a b n : is_Some (L a) → ✓{n}(a ⋅ b) → L (a ⋅ b) ≡{n}≡ (L a) ⋅ Some b
-  }.
-
-  Definition local_update_op (b : A) : LocalUpdate
-    := λ a, Some (b ⋅ a).
-  Global Instance local_update_op_spec b : LocalUpdateSpec (local_update_op b).
-  Proof.
-    rewrite /local_update_op. split.
-    - move=>? ? ? EQ /=. by rewrite EQ.
-    - move=>a a' n Hlv Hv /=. by rewrite associative.
-  Qed.
-End local_update.
-Arguments LocalUpdate : clear implicits.
-
-
diff --git a/program_logic/auth.v b/program_logic/auth.v
index ec2496b552c9220cb6ef86786e04dea3c876ea4a..d5f62fbc425229b24511ab696c15e0e5c7ca2301 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -14,16 +14,16 @@ Section auth.
   (* TODO: Need this to be proven somewhere. *)
   (* FIXME ✓ binds too strong, I need parenthesis here. *)
   Hypothesis auth_valid :
-    forall a b, (✓(Auth (Excl a) b) : iProp Λ (globalC Σ)) ⊑ (∃ b', a ≡ b ⋅ b').
+    forall a b, (✓ (Auth (Excl a) b) : iProp Λ (globalC Σ)) ⊑ (∃ b', a ≡ b ⋅ b').
 
   (* FIXME how much would break if we had a global instance from ∅ to Inhabited? *)
   Local Instance auth_inhabited : Inhabited A.
   Proof. split. exact ∅. Qed.
 
   Definition auth_inv (γ : gname) : iProp Λ (globalC Σ) :=
-    (∃ a, own AuthI γ (●a) ★ φ a)%I.
-  Definition auth_own (γ : gname) (a : A) := own AuthI γ (◯a).
-  Definition auth_ctx (γ : gname) := inv N (auth_inv γ).
+    (∃ a, own AuthI γ (● a) ★ φ a)%I.
+  Definition auth_own (γ : gname) (a : A) : iProp Λ (globalC Σ) := own AuthI γ (◯ a).
+  Definition auth_ctx (γ : gname) : iProp Λ (globalC Σ) := inv N (auth_inv γ).
 
   Lemma auth_alloc a :
     ✓a → φ a ⊑ pvs N N (∃ γ, auth_ctx γ ∧ auth_own γ a).
@@ -58,18 +58,15 @@ Section auth.
     by rewrite sep_elim_l.
   Qed.
 
-  Context (L : LocalUpdate A) `{!LocalUpdateSpec L}.
-  Lemma auth_closing  a a' b γ :
-    L a = Some b → ✓(b ⋅ a') →
-    (φ (b ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
-      ⊑ pvs N N (auth_inv γ ★ auth_own γ b).
+  Lemma auth_closing `{!LocalUpdate φf f} a a' γ :
+    φf a → ✓ (f a ⋅ a') →
+    (φ (f a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
+    ⊑ pvs N N (auth_inv γ ★ auth_own γ (f a)).
   Proof.
-    intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (b â‹… a')).
+    intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (f a â‹… a')).
     rewrite [(_ ★ φ _)%I]commutative -associative.
-    rewrite -pvs_frame_l. apply sep_mono; first done.
-    rewrite -own_op. apply own_update.
-    by apply (auth_local_update L).
+    rewrite -pvs_frame_l -own_op; apply sep_mono; first done.
+    by apply own_update, (auth_local_update_l f).
   Qed.
 
 End auth.
-