diff --git a/algebra/cmra.v b/algebra/cmra.v
index 84f6ea44913783ceb765c27208d0be0416d5c403..75c08848036832353a71d178eb8d5bbf8cff5556 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -393,6 +393,35 @@ Section cmra_monotone.
   Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
 End cmra_monotone.
 
+(** * Transporting a CMRA equality *)
+Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
+  eq_rect A id x _ H.
+
+Section cmra_transport.
+  Context {A B : cmraT} (H : A = B).
+  Notation T := (cmra_transport H).
+  Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T.
+  Proof. by intros ???; destruct H. Qed.
+  Global Instance cmra_transport_proper : Proper ((≡) ==> (≡)) T.
+  Proof. by intros ???; destruct H. Qed.
+  Lemma cmra_transport_op x y : T (x â‹… y) = T x â‹… T y.
+  Proof. by destruct H. Qed.
+  Lemma cmra_transport_unit x : T (unit x) = unit (T x).
+  Proof. by destruct H. Qed.
+  Lemma cmra_transport_validN n x : ✓{n} (T x) ↔ ✓{n} x.
+  Proof. by destruct H. Qed.
+  Lemma cmra_transport_valid x : ✓ (T x) ↔ ✓ x.
+  Proof. by destruct H. Qed.
+  Global Instance cmra_transport_timeless x : Timeless x → Timeless (T x).
+  Proof. by destruct H. Qed.
+  Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x :
+    x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
+  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
+  Lemma cmra_transport_updateP' (P : A → Prop) x :
+    x ~~>: P → T x ~~>: λ y, ∃ y', y = cmra_transport H y' ∧ P y'.
+  Proof. eauto using cmra_transport_updateP. Qed.
+End cmra_transport.
+
 (** * Instances *)
 (** ** Discrete CMRA *)
 Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 2a5afdf23d1b4623607fa2c60a237b4ecbaf0e60..1feea5ec5525bd8896b8d0eae99328c032ece24b 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -3,8 +3,8 @@ Require Import algebra.functor.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
+Implicit Types m : gmap K A.
 
-(* COFE *)
 Instance map_dist : Dist (gmap K A) := λ n m1 m2,
   ∀ i, m1 !! i ={n}= m2 !! i.
 Program Definition map_chain (c : chain (gmap K A))
@@ -36,44 +36,45 @@ 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 insert_ne (i : K) n :
+Global Instance insert_ne i n :
   Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
 Proof.
   intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
     [by constructor|by apply lookup_ne].
 Qed.
-Global Instance singleton_ne (i : K) n :
+Global Instance singleton_ne i n :
   Proper (dist n ==> dist n) (singletonM i : A → gmap K A).
 Proof. by intros ???; apply insert_ne. Qed.
-Global Instance delete_ne (i : K) n :
+Global Instance delete_ne i n :
   Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
 Proof.
   intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
     [by constructor|by apply lookup_ne].
 Qed.
+
 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.
 Qed.
-Global Instance map_lookup_timeless (m : gmap K A) i :
-  Timeless m → Timeless (m !! i).
+Global Instance map_lookup_timeless m i : Timeless m → Timeless (m !! i).
 Proof.
   intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
   assert (m ={1}= <[i:=x]> m)
     by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
   by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
 Qed.
-Global Instance map_insert_timeless (m : gmap K A) i x :
+Global Instance map_insert_timeless m i x :
   Timeless x → Timeless m → Timeless (<[i:=x]>m).
 Proof.
   intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality.
   { by apply (timeless _); rewrite -Hm lookup_insert. }
   by apply (timeless _); rewrite -Hm lookup_insert_ne.
 Qed.
-Global Instance map_singleton_timeless (i : K) (x : A) :
+Global Instance map_singleton_timeless i x :
   Timeless x → Timeless ({[ i ↦ x ]} : gmap K A) := _.
 End cofe.
+
 Arguments mapC _ {_ _} _.
 
 (* CMRA *)
@@ -84,12 +85,14 @@ Instance map_op : Op (gmap K A) := merge op.
 Instance map_unit : Unit (gmap K A) := fmap unit.
 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.
 Proof. by apply lookup_merge. Qed.
 Lemma lookup_minus m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i.
 Proof. by apply lookup_merge. Qed.
 Lemma lookup_unit m i : unit m !! i = unit (m !! i).
 Proof. by apply lookup_fmap. Qed.
+
 Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
 Proof.
   split.
@@ -105,6 +108,7 @@ Proof.
   * intros Hm; exists (m2 ⩪ m1); intros i.
     by rewrite lookup_op lookup_minus cmra_op_minus.
 Qed.
+
 Definition map_cmra_mixin : CMRAMixin (gmap K A).
 Proof.
   split.
@@ -152,35 +156,32 @@ Proof.
   * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
   * apply map_empty_timeless.
 Qed.
-
 End cmra.
+
 Arguments mapRA _ {_ _} _.
 
 Section properties.
-Context `{Countable K} {A: cmraT}.
+Context `{Countable K} {A : cmraT}.
 Implicit Types m : gmap K A.
+Implicit Types i : K.
+Implicit Types a : A.
 
 Lemma map_lookup_validN n m i x : ✓{n} m → m !! i ={n}= Some x → ✓{n} x.
 Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
 Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} (<[i:=x]>m).
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
+Lemma map_singleton_validN n i x : ✓{n} ({[ i ↦ x ]} : gmap K A) ↔ ✓{n} x.
+Proof.
+  split; [|by intros; apply map_insert_validN, cmra_empty_valid].
+  by move=>/(_ i); simplify_map_equality.
+Qed.
 
 Lemma map_insert_op m1 m2 i x :
   m2 !! i = None → <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2.
 Proof. by intros Hi; apply (insert_merge_l _ m1 m2); rewrite Hi. Qed.
-
-Lemma map_validN_singleton n (i : K) (x : A) :
-  ✓{n} x <-> ✓{n} ({[ i ↦ x ]} : gmap K A).
-Proof.
-  split.
-  - move=>Hx j. destruct (decide (i = j)); simplify_map_equality; done.
-  - move=>Hm. move: (Hm i). by simplify_map_equality.
-Qed.
-
 Lemma map_unit_singleton (i : K) (x : A) :
   unit ({[ i ↦ x ]} : gmap K A) = {[ i ↦ unit x ]}.
 Proof. apply map_fmap_singleton. Qed.
-
 Lemma map_op_singleton (i : K) (x y : A) :
   {[ i ↦ x ]} ⋅ {[ i ↦ y ]} = ({[ i ↦ x ⋅ y ]} : gmap K A).
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
@@ -220,7 +221,7 @@ Lemma map_insert_updateP' (P : A → Prop) m i x :
 Proof. eauto using map_insert_updateP. Qed.
 Lemma map_insert_update m i x y : x ~~> y → <[i:=x]>m ~~> <[i:=y]>m.
 Proof.
-  rewrite !cmra_update_updateP; eauto using map_insert_updateP with congruence.
+  rewrite !cmra_update_updateP; eauto using map_insert_updateP with subst.
 Qed.
 
 Lemma map_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x :
@@ -228,13 +229,9 @@ Lemma map_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x :
 Proof. apply map_insert_updateP. Qed.
 Lemma map_singleton_updateP' (P : A → Prop) i x :
   x ~~>: P → {[ i ↦ x ]} ~~>: λ m', ∃ y, m' = {[ i ↦ y ]} ∧ P y.
-Proof. eauto using map_singleton_updateP. Qed.
+Proof. apply map_insert_updateP'. Qed.
 Lemma map_singleton_update i (x y : A) : x ~~> y → {[ i ↦ x ]} ~~> {[ i ↦ y ]}.
-Proof.
-  rewrite !cmra_update_updateP=>?. eapply map_singleton_updateP; first eassumption.
-  by move=>? ->.
-Qed.
-
+Proof. apply map_insert_update. Qed.
 
 Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
 Lemma map_updateP_alloc (Q : gmap K A → Prop) m x :
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 47e590c19b6879b6c9296e7bdc870fd31a105437..211f92f3d83cc5b9af8a89b3ad1088a5d4a3d691 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -1,22 +1,25 @@
 Require Export algebra.cmra.
 Require Import algebra.functor.
 
-(** Indexed product *)
+(** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
 Definition iprod {A} (B : A → cofeT) := ∀ x, B x.
-Definition iprod_insert `{∀ x x' : A, Decision (x = x')} {B : A → cofeT}
+Definition iprod_insert {A} {B : A → cofeT} `{∀ x x' : A, Decision (x = x')}
     (x : A) (y : B x) (f : iprod B) : iprod B := λ x',
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
-Global Instance iprod_empty {A} {B : A → cofeT} `{∀ x, Empty (B x)} : Empty (iprod B) := λ x, ∅.
-Definition iprod_lookup_empty {A} {B : A → cofeT} `{∀ x, Empty (B x)} x : ∅ x = ∅ := eq_refl.
-Definition iprod_singleton
-    `{∀ x x' : A, Decision (x = x')} {B : A → cofeT} `{∀ x : A, Empty (B x)}
+Global Instance iprod_empty {A} {B : A → cofeT}
+  `{∀ x, Empty (B x)} : Empty (iprod B) := λ x, ∅.
+Definition iprod_singleton {A} {B : A → cofeT} 
+    `{∀ x x' : A, Decision (x = x'), ∀ x : A, Empty (B x)}
   (x : A) (y : B x) : iprod B := iprod_insert x y ∅.
+Instance: Params (@iprod_insert) 4.
+Instance: Params (@iprod_singleton) 5.
 
 Section iprod_cofe.
   Context {A} {B : A → cofeT}.
   Implicit Types x : A.
   Implicit Types f g : iprod B.
+
   Instance iprod_equiv : Equiv (iprod B) := λ f g, ∀ x, f x ≡ g x.
   Instance iprod_dist : Dist (iprod B) := λ n f g, ∀ x, f x ={n}= g x.
   Program Definition iprod_chain (c : chain (iprod B)) (x : A) : chain (B x) :=
@@ -41,6 +44,15 @@ Section iprod_cofe.
   Qed.
   Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin.
 
+  (** Properties of empty *)
+  Section empty.
+    Context `{∀ x, Empty (B x)}.
+    Definition iprod_lookup_empty  x : ∅ x = ∅ := eq_refl.
+    Instance iprod_empty_timeless :
+      (∀ x : A, Timeless (∅ : B x)) → Timeless (∅ : iprod B).
+    Proof. intros ? f Hf x. by apply (timeless _). Qed.
+  End empty.
+
   (** Properties of iprod_insert. *)
   Context `{∀ x x' : A, Decision (x = x')}.
 
@@ -50,7 +62,6 @@ Section iprod_cofe.
     intros y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
     by destruct (decide _) as [[]|].
   Qed.
-
   Global Instance iprod_insert_proper x :
     Proper ((≡) ==> (≡) ==> (≡)) (iprod_insert x) := ne_proper_2 _.
 
@@ -59,90 +70,62 @@ Section iprod_cofe.
     rewrite /iprod_insert; destruct (decide _) as [Hx|]; last done.
     by rewrite (proof_irrel Hx eq_refl).
   Qed.
-
   Lemma iprod_lookup_insert_ne f x x' y :
     x ≠ x' → (iprod_insert x y f) x' = f x'.
   Proof. by rewrite /iprod_insert; destruct (decide _). Qed.
 
-  Global Instance iprod_lookup_timeless f x :
-    Timeless f → Timeless (f x).
+  Global Instance iprod_lookup_timeless f x : Timeless f → Timeless (f x).
   Proof.
-    intros ? y Hf.
+    intros ? y ?.
     cut (f ≡ iprod_insert x y f).
-    { move=>{Hf} Hf. by rewrite (Hf x) iprod_lookup_insert. }
-    apply timeless; first by apply _.
-    move=>x'. destruct (decide (x = x')).
-    - subst x'. rewrite iprod_lookup_insert; done.
-    - rewrite iprod_lookup_insert_ne //.
+    { by move=> /(_ x)->; rewrite iprod_lookup_insert. }
+    by apply (timeless _)=>x'; destruct (decide (x = x')) as [->|];
+      rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
   Qed.
-
   Global Instance iprod_insert_timeless f x y :
     Timeless f → Timeless y → Timeless (iprod_insert x y f).
   Proof.
-    intros ?? g Heq x'. destruct (decide (x = x')).
-    - subst x'. rewrite iprod_lookup_insert.
-      apply (timeless _).
-      rewrite -(Heq x) iprod_lookup_insert; done.
-    - rewrite iprod_lookup_insert_ne //.
-      apply (timeless _).
-      rewrite -(Heq x') iprod_lookup_insert_ne; done.
+    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
+    * rewrite iprod_lookup_insert.
+      apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert.
+    * rewrite iprod_lookup_insert_ne //.
+      apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert_ne.
   Qed.
 
   (** Properties of iprod_singletom. *)
   Context `{∀ x : A, Empty (B x)}.
+
   Global Instance iprod_singleton_ne x n :
     Proper (dist n ==> dist n) (iprod_singleton x).
   Proof. by intros y1 y2 Hy; rewrite /iprod_singleton Hy. Qed.
   Global Instance iprod_singleton_proper x :
     Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _.
+
   Lemma iprod_lookup_singleton x y : (iprod_singleton x y) x = y.
   Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
-  Lemma iprod_lookup_singleton_ne x x' y :
-    x ≠ x' → (iprod_singleton x y) x' = ∅.
+  Lemma iprod_lookup_singleton_ne x x' y: x ≠ x' → (iprod_singleton x y) x' = ∅.
   Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
 
-  Context `{∀ x : A, Timeless (∅ : B x)}.
-  Instance iprod_empty_timeless : Timeless (∅ : iprod B).
-  Proof. intros f Hf x. by apply (timeless _). Qed.
-
   Global Instance iprod_singleton_timeless x (y : B x) :
-    Timeless y → Timeless (iprod_singleton x y) := _.
-
+    (∀ x : A, Timeless (∅ : B x)) → Timeless y → Timeless (iprod_singleton x y).
+  Proof. eauto using iprod_insert_timeless, iprod_empty_timeless. Qed.
 End iprod_cofe.
 
 Arguments iprodC {_} _.
 
-Definition iprod_map {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
-  (g : iprod B1) : iprod B2 := λ x, f _ (g x).
-Lemma iprod_map_ext {A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) g :
-  (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
-Proof. done. Qed.
-Lemma iprod_map_id {A} {B: A → cofeT} (g : iprod B) : iprod_map (λ _, id) g = g.
-Proof. done. Qed.
-Lemma iprod_map_compose {A} {B1 B2 B3 : A → cofeT}
-    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
-  iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
-Proof. done. Qed.
-Instance iprod_map_ne {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n :
-  (∀ x, Proper (dist n ==> dist n) (f x)) →
-  Proper (dist n ==> dist n) (iprod_map f).
-Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
-Definition iprodC_map {A} {B1 B2 : A → cofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
-  iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
-Instance iprodC_map_ne {A} {B1 B2 : A → cofeT} n :
-  Proper (dist n ==> dist n) (@iprodC_map A B1 B2).
-Proof. intros f1 f2 Hf g x; apply Hf. Qed.
-
 Section iprod_cmra.
   Context {A} {B : A → cmraT}.
   Implicit Types f g : iprod B.
+
   Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
-  Definition iprod_lookup_op f g x : (f â‹… g) x = f x â‹… g x := eq_refl.
   Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
-  Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
   Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} (f x).
   Instance iprod_minus : Minus (iprod B) := λ f g x, f x ⩪ g x.
+
+  Definition iprod_lookup_op f g x : (f â‹… g) x = f x â‹… g x := eq_refl.
+  Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
   Definition iprod_lookup_minus f g x : (f ⩪ g) x = f x ⩪ g x := eq_refl.
+
   Lemma iprod_includedN_spec (f g : iprod B) n : f ≼{n} g ↔ ∀ x, f x ≼{n} g x.
   Proof.
     split.
@@ -150,6 +133,7 @@ Section iprod_cmra.
     * intros Hh; exists (g ⩪ f)=> x; specialize (Hh x).
       by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus.
   Qed.
+
   Definition iprod_cmra_mixin : CMRAMixin (iprod B).
   Proof.
     split.
@@ -209,31 +193,27 @@ Section iprod_cmra.
   Lemma iprod_insert_update g x y1 y2 :
     y1 ~~> y2 → iprod_insert x y1 g ~~> iprod_insert x y2 g.
   Proof.
-    rewrite !cmra_update_updateP;
-      eauto using iprod_insert_updateP with congruence.
+    rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
   Qed.
 
   (** Properties of iprod_singleton. *)
-  Context `{∀ x, Empty (B x)} `{∀ x, CMRAIdentity (B x)}.
+  Context `{∀ x, Empty (B x), ∀ x, CMRAIdentity (B x)}.
 
-  Lemma iprod_validN_singleton n x (y : B x) :
-    ✓{n} y <-> ✓{n} (iprod_singleton x y).
+  Lemma iprod_singleton_validN n x (y : B x) :
+    ✓{n} (iprod_singleton x y) ↔ ✓{n} y.
   Proof.
-    split.
-    - move=>Hx x'. destruct (decide (x = x')).
-      + subst x'. by rewrite iprod_lookup_singleton.
-      + rewrite iprod_lookup_singleton_ne //; [].
-        by apply cmra_empty_valid.
-    - move=>Hm. move: (Hm x). by rewrite iprod_lookup_singleton.
+    split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
+    move=>Hx x'; destruct (decide (x = x')) as [->|];
+      rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
+    by apply cmra_empty_valid.
   Qed.
 
   Lemma iprod_unit_singleton x (y : B x) :
     unit (iprod_singleton x y) ≡ iprod_singleton x (unit y).
   Proof.
-    move=>x'. rewrite iprod_lookup_unit. destruct (decide (x = x')).
-    - subst x'. by rewrite !iprod_lookup_singleton.
-    - rewrite !iprod_lookup_singleton_ne //; [].
-      by apply cmra_unit_empty.
+    by move=>x'; destruct (decide (x = x')) as [->|];
+      rewrite iprod_lookup_unit ?iprod_lookup_singleton
+      ?iprod_lookup_singleton_ne // cmra_unit_empty.
   Qed.
 
   Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
@@ -248,32 +228,45 @@ Section iprod_cmra.
     y1 ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) →
     iprod_singleton x y1 ~~>: Q.
   Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP. Qed.
-
   Lemma iprod_singleton_updateP' x (P : B x → Prop) y1 :
     y1 ~~>: P →
     iprod_singleton x y1 ~~>: λ g', ∃ y2, g' = iprod_singleton x y2 ∧ P y2.
   Proof. eauto using iprod_singleton_updateP. Qed.
+  Lemma iprod_singleton_update x y1 y2 :
+    y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2.
+  Proof. eauto using iprod_insert_update. Qed.
 
   Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) :
-    (∅ ~~>: P) → (∀ y2, P y2 → Q (iprod_singleton x y2)) →
-    ∅ ~~>: Q.
+    ∅ ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ∅ ~~>: Q.
   Proof.
-    intros Hx HQ gf n Hg. destruct (Hx (gf x) n) as (y2&?&?).
-    { apply: Hg. }
-    exists (iprod_singleton x y2).
-    split; first by apply HQ.
-    intros x'; destruct (decide (x' = x)) as [->|];
-      rewrite iprod_lookup_op /iprod_singleton ?iprod_lookup_insert //; [].
-    move:(Hg x'). by rewrite iprod_lookup_insert_ne // left_id.
+    intros Hx HQ gf n Hg. destruct (Hx (gf x) n) as (y2&?&?); first apply Hg.
+    exists (iprod_singleton x y2); split; [by apply HQ|].
+    intros x'; destruct (decide (x' = x)) as [->|].
+    * by rewrite iprod_lookup_op iprod_lookup_singleton.
+    * rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
   Qed.
-
-  Lemma iprod_singleton_update x y1 y2 :
-    y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2.
-  Proof. by intros; apply iprod_insert_update. Qed.
 End iprod_cmra.
 
 Arguments iprodRA {_} _.
 
+(** * Functor *)
+Definition iprod_map {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
+  (g : iprod B1) : iprod B2 := λ x, f _ (g x).
+
+Lemma iprod_map_ext {A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) g :
+  (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
+Proof. done. Qed.
+Lemma iprod_map_id {A} {B: A → cofeT} (g : iprod B) : iprod_map (λ _, id) g = g.
+Proof. done. Qed.
+Lemma iprod_map_compose {A} {B1 B2 B3 : A → cofeT}
+    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
+  iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
+Proof. done. Qed.
+
+Instance iprod_map_ne {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n :
+  (∀ x, Proper (dist n ==> dist n) (f x)) →
+  Proper (dist n ==> dist n) (iprod_map f).
+Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
 Instance iprod_map_cmra_monotone {A} {B1 B2: A → cmraT} (f : ∀ x, B1 x → B2 x) :
   (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f).
 Proof.
@@ -283,6 +276,12 @@ Proof.
   * intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg.
 Qed.
 
+Definition iprodC_map {A} {B1 B2 : A → cofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
+  iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
+Instance iprodC_map_ne {A} {B1 B2 : A → cofeT} n :
+  Proper (dist n ==> dist n) (@iprodC_map A B1 B2).
+Proof. intros f1 f2 Hf g x; apply Hf. Qed.
+
 Program Definition iprodF {A} (Σ : A → iFunctor) : iFunctor := {|
   ifunctor_car B := iprodRA (λ x, Σ x B);
   ifunctor_map B1 B2 f := iprodC_map (λ x, ifunctor_map (Σ x) f);
diff --git a/heap_lang/sugar.v b/heap_lang/sugar.v
index 19c8ae5e68388aadf87e6ac828e5161e91e288fa..f848169f5485afa82b55ca98c5c6ed4a5c1944ef 100644
--- a/heap_lang/sugar.v
+++ b/heap_lang/sugar.v
@@ -29,7 +29,7 @@ Module notations.
   (* What about Arguments for hoare triples?. *)
   (* The colons indicate binders. "let" is not consistent here though,
      thing are only bound in the "in". *)
-  Notation "# n" := (Var n) (at level 1, format "# n") : lang_scope.
+  Notation "# n" := (ids (term:=expr) n) (at level 1, format "# n") : lang_scope.
   Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
   Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
   Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
@@ -41,10 +41,12 @@ Module notations.
   Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope.
   (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
   Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
-  Notation "e1 ; e2" := (Seq e1%L e2%L) (at level 100) : lang_scope.
-  Notation "'let:' e1 'in' e2" := (Let e1%L e2%L) (at level 102) : lang_scope.
-  Notation "'λ:' e" := (Lam e%L) (at level 102) : lang_scope.
-  Notation "'rec::' e" := (Rec e%L) (at level 102) : lang_scope.
+  Notation "e1 ; e2" := (Seq e1%L e2%L)
+    (at level 100, e2 at level 200) : lang_scope.
+  Notation "'let:' e1 'in' e2" := (Let e1%L e2%L)
+    (at level 102, e2 at level 200) : lang_scope.
+  Notation "'λ:' e" := (Lam e%L) (at level 102, e at level 200) : lang_scope.
+  Notation "'rec::' e" := (Rec e%L) (at level 102, e at level 200) : lang_scope.
   Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
     (at level 200, e1, e2, e3 at level 200) : lang_scope.
 End notations.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 570f58a4caf6a20c77e666407edded89d635ce08..fc2ba165803c9c17812191dd62e530b666fc1c35 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -53,16 +53,15 @@ Module LiftingTests.
   (* TODO: once asimpl preserves notation, we don't need
      FindPred' anymore. *)
   (* FIXME: fix notation so that we do not need parenthesis or %L *)
-  Definition FindPred' n1 Sn1 n2 f : expr :=
+  Definition FindPred' (n1 Sn1 n2 f : expr) : expr :=
     if Sn1 < n2 then f Sn1 else n1.
-  Definition FindPred n2 : expr :=
+  Definition FindPred (n2 : expr) : expr :=
     rec:: (let: #1 + Lit 1 in FindPred' #2 #0 n2.[ren(+3)] #1)%L.
   Definition Pred : expr :=
     λ: (if #0 ≤ Lit 0 then Lit 0 else FindPred #0 (Lit 0))%L.
 
   Lemma FindPred_spec n1 n2 E Q :
-    (■(n1 < n2) ∧ Q $ LitV (pred n2)) ⊑
-       wp E (FindPred (Lit n2) (Lit n1)) Q.
+    (■ (n1 < n2) ∧ Q (LitV $ pred n2)) ⊑ wp E (FindPred (Lit n2) (Lit n1)) Q.
   Proof.
     revert n1. apply löb_all_1=>n1.
     rewrite -wp_rec //. asimpl.
@@ -70,8 +69,12 @@ Module LiftingTests.
     etransitivity; first (etransitivity; last eapply equiv_spec, later_and).
     { apply and_mono; first done. by rewrite -later_intro. }
     apply later_mono.
-    (* Go on. *)
-    rewrite -(wp_let _ _ (FindPred' (Lit n1) #0 (Lit n2) (FindPred (Lit n2)))).
+    (* Go on *)
+    (* FIXME "rewrite -(wp_let _ _ (FindPred' n1 #0 n2 (FindPred n2)))" started to
+    fail after we changed # n to use ids instead of Var *)
+    pose proof (wp_let (Σ:=Σ) E (Lit n1 + Lit 1)%L
+                   (FindPred' (Lit n1) #0 (Lit n2) (FindPred (Lit n2))) Q).
+    unfold Let, Lam in H; rewrite -H.
     rewrite -wp_bin_op //. asimpl.
     rewrite -(wp_bindi (IfCtx _ _)).
     rewrite -!later_intro /=.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index d5867ab6d90799e057fcc031ce9dc682005944e1..8a0551fb89a73076b660765f8e0069dca927cd15 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -26,10 +26,12 @@ Hint Extern 998 (_ = _) => f_equal : f_equal.
 Hint Extern 999 => congruence : congruence.
 Hint Extern 1000 => lia : lia.
 Hint Extern 1000 => omega : omega.
+Hint Extern 1001 => progress subst : subst. (** backtracking on this one will
+be very bad, so use with care! *)
 
 (** The tactic [intuition] expands to [intuition auto with *] by default. This
 is rather efficient when having big hint databases, or expensive [Hint Extern]
-declarations as the above. *)
+declarations as the ones above. *)
 Tactic Notation "intuition" := intuition auto.
 
 (** A slightly modified version of Ssreflect's finishing tactic [done]. It
diff --git a/program_logic/global_cmra.v b/program_logic/global_cmra.v
index 326110b65c9a7531f03e8ca5b1413520ec3e5ac7..f340c56f79514b426670e31629c2de88882fb22f 100644
--- a/program_logic/global_cmra.v
+++ b/program_logic/global_cmra.v
@@ -6,144 +6,89 @@ Definition gid := positive.
 Definition globalC (Σ : gid → iFunctor) : iFunctor :=
   iprodF (λ i, mapF gid (Σ i)).
 
-Class InG Λ (Σ : gid → iFunctor) (i : gid) (A : cmraT) :=
+Class InG (Λ : language) (Σ : gid → iFunctor) (i : gid) (A : cmraT) :=
   inG : A = Σ i (laterC (iPreProp Λ (globalC Σ))).
 
+Definition to_globalC {Λ Σ A}
+    (i : gid) `{!InG Λ Σ i A} (γ : gid) (a : A) : iGst Λ (globalC Σ) :=
+  iprod_singleton i {[ γ ↦ cmra_transport inG a ]}.
+Definition own {Λ Σ A}
+    (i : gid) `{!InG Λ Σ i A} (γ : gid) (a : A) : iProp Λ (globalC Σ) :=
+  ownG (to_globalC i γ a).
+Instance: Params (@to_globalC) 6.
+Instance: Params (@own) 6.
+Typeclasses Opaque to_globalC own.
+
 Section global.
 Context {Λ : language} {Σ : gid → iFunctor} (i : gid) `{!InG Λ Σ i A}.
 Implicit Types a : A.
 
-Definition to_Σ (a : A) : Σ i (laterC (iPreProp Λ (globalC Σ))) :=
-  eq_rect A id a _ inG.
-Definition to_globalC (γ : gid) `{!InG Λ Σ i A} (a : A) : iGst Λ (globalC Σ) :=
-  iprod_singleton i {[ γ ↦ to_Σ a ]}.
-Definition own (γ : gid) (a : A) : iProp Λ (globalC Σ) :=
-  ownG (to_globalC γ a).
-
-Definition from_Σ (b : Σ i (laterC (iPreProp Λ (globalC Σ)))) : A  :=
-  eq_rect (Σ i _) id b _ (Logic.eq_sym inG).
-Definition P_to_Σ (P : A → Prop) (b : Σ i (laterC (iPreProp Λ (globalC Σ)))) : Prop
-  := P (from_Σ b).
-
-(* Properties of the transport. *)
-Lemma to_from_Σ b :
-  to_Σ (from_Σ b) = b.
-Proof.
-  rewrite /to_Σ /from_Σ. by destruct inG.
-Qed.
-
 (* Properties of to_globalC *)
-Lemma globalC_op γ a1 a2 :
-  to_globalC γ (a1 ⋅ a2) ≡ to_globalC γ a1 ⋅ to_globalC γ a2.
-Proof.
-  rewrite /to_globalC iprod_op_singleton map_op_singleton.
-  apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
-  by rewrite /to_Σ; destruct inG.
-Qed.
-
-Lemma globalC_validN n γ a :
-  ✓{n} (to_globalC γ a) <-> ✓{n} a.
+Instance to_globalC_ne γ n : Proper (dist n ==> dist n) (to_globalC i γ).
+Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
+Lemma to_globalC_validN n γ a : ✓{n} (to_globalC i γ a) ↔ ✓{n} a.
 Proof.
-  rewrite /to_globalC.
-  rewrite -iprod_validN_singleton -map_validN_singleton.
-  by rewrite /to_Σ; destruct inG.
+  by rewrite /to_globalC
+    iprod_singleton_validN map_singleton_validN cmra_transport_validN.
 Qed.
-
-Lemma globalC_unit γ a :
-  unit (to_globalC γ a) ≡ to_globalC γ (unit a).
+Lemma to_globalC_op γ a1 a2 :
+  to_globalC i γ (a1 ⋅ a2) ≡ to_globalC i γ a1 ⋅ to_globalC i γ a2.
 Proof.
-  rewrite /to_globalC.
-  rewrite iprod_unit_singleton map_unit_singleton.
-  apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
-  by rewrite /to_Σ; destruct inG.
+  by rewrite /to_globalC iprod_op_singleton map_op_singleton cmra_transport_op.
 Qed.
-
-Global Instance globalC_timeless γ m : Timeless m → Timeless (to_globalC γ m).
+Lemma to_globalC_unit γ a : unit (to_globalC i γ a) ≡ to_globalC i γ (unit a).
 Proof.
-  rewrite /to_globalC => ?.
-  apply iprod_singleton_timeless, map_singleton_timeless.
-  by rewrite /to_Σ; destruct inG.
+  by rewrite /to_globalC
+    iprod_unit_singleton map_unit_singleton cmra_transport_unit.
 Qed.
-
-(* Properties of the lifted frame-preserving updates *)
-Lemma update_to_Σ a P :
-  a ~~>: P → to_Σ a ~~>: P_to_Σ P.
-Proof.
-  move=>Hu gf n Hf. destruct (Hu (from_Σ gf) n) as [a' Ha'].
-  { move: Hf. rewrite /to_Σ /from_Σ. by destruct inG. }
-  exists (to_Σ a'). move:Hf Ha'.
-  rewrite /P_to_Σ /to_Σ /from_Σ. destruct inG. done.
-Qed. 
+Instance to_globalC_timeless γ m : Timeless m → Timeless (to_globalC i γ m).
+Proof. rewrite /to_globalC; apply _. Qed.
 
 (* Properties of own *)
-
-Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
+Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
+Proof. by intros m m' Hm; rewrite /own Hm. Qed.
+Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper _.
+
+Lemma own_op γ a1 a2 : own i γ (a1 ⋅ a2) ≡ (own i γ a1 ★ own i γ a2)%I.
+Proof. by rewrite /own -ownG_op to_globalC_op. Qed.
+Lemma always_own_unit γ a : (□ own i γ (unit a))%I ≡ own i γ (unit a).
+Proof. by rewrite /own -to_globalC_unit always_ownG_unit. Qed.
+Lemma own_valid γ a : own i γ a ⊑ ✓ a.
 Proof.
-  intros m m' Hm; apply ownG_ne, iprod_singleton_ne, singleton_ne.
-  by rewrite /to_globalC /to_Σ; destruct inG.
+  rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalC_validN.
 Qed.
-
-Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own γ) := ne_proper _.
-
-Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ≡ (own γ a1 ★ own γ a2)%I.
-Proof. rewrite /own -ownG_op. apply ownG_proper, globalC_op. Qed.
-
-(* TODO: This also holds if we just have ✓a at the current step-idx, as Iris
-   assertion. However, the map_updateP_alloc does not suffice to show this. *)
-Lemma own_alloc E a :
-  ✓a → True ⊑ pvs E E (∃ γ, own γ a).
-Proof.
-  intros Ha. set (P m := ∃ γ, m = to_globalC γ a).
-  rewrite -(pvs_mono _ _ (∃ m, ■P m ∧ ownG m)%I).
-  - rewrite -pvs_ownG_updateP_empty //; [].
-    subst P. eapply (iprod_singleton_updateP_empty i).
-    + apply map_updateP_alloc' with (x:=to_Σ a).
-      by rewrite /to_Σ; destruct inG.
-    + simpl. move=>? [γ [-> ?]]. exists γ. done.
-  - apply exist_elim=>m. apply const_elim_l=>-[p ->] {P}.
-    by rewrite -(exist_intro p).
-Qed.
-
-Lemma always_own_unit γ a : (□ own γ (unit a))%I ≡ own γ (unit a).
-Proof. rewrite /own -globalC_unit. by apply always_ownG_unit. Qed.
-
-Lemma own_valid γ a : (own γ a) ⊑ (✓ a).
-Proof.
-  rewrite /own ownG_valid. apply uPred.valid_mono=>n.
-  by apply globalC_validN.
-Qed.
-
-Lemma own_valid_r' γ a : (own γ a) ⊑ (own γ a ★ ✓ a).
+Lemma own_valid_r' γ a : own i γ a ⊑ (own i γ a ★ ✓ a).
 Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
+Global Instance own_timeless γ a : Timeless a → TimelessP (own i γ a).
+Proof. unfold own; apply _. Qed.
 
-Global Instance ownG_timeless γ a : Timeless a → TimelessP (own γ a).
+(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
+   assertion. However, the map_updateP_alloc does not suffice to show this. *)
+Lemma own_alloc E a : ✓ a → True ⊑ pvs E E (∃ γ, own i γ a).
 Proof.
-  intros. apply ownG_timeless. apply _.
+  intros Ha.
+  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, m = to_globalC i γ a) ∧ ownG m)%I).
+  * eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty i);
+      first (eapply map_updateP_alloc', cmra_transport_valid, Ha); naive_solver.
+  * apply exist_elim=>m; apply const_elim_l=>-[γ ->].
+    by rewrite -(exist_intro γ).
 Qed.
 
 Lemma pvs_updateP E γ a P :
-  a ~~>: P → own γ a ⊑ pvs E E (∃ a', ■ P a' ∧ own γ a').
+  a ~~>: P → own i γ a ⊑ pvs E E (∃ a', ■ P a' ∧ own i γ a').
 Proof.
-  intros Ha. set (P' m := ∃ a', P a' ∧ m = to_globalC γ a').
-  rewrite -(pvs_mono _ _ (∃ m, ■P' m ∧ ownG m)%I).
-  - rewrite -pvs_ownG_updateP; first by rewrite /own.
-    rewrite /to_globalC. eapply iprod_singleton_updateP.
-    + (* FIXME RJ: I tried apply... with instead of instantiate, that
-         does not work. *)
-      apply map_singleton_updateP'. instantiate (1:=P_to_Σ P).
-      by apply update_to_Σ.
-    + simpl. move=>? [y [-> HP]]. exists (from_Σ y). split.
-      * move: HP. rewrite /P_to_Σ /from_Σ. by destruct inG.
-      * clear HP. rewrite /to_globalC to_from_Σ; done.
-  - apply exist_elim=>m. apply const_elim_l=>-[a' [HP ->]].
-    rewrite -(exist_intro a'). apply and_intro; last done.
-    by apply const_intro.
+  intros Ha.
+  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ b, m = to_globalC i γ b ∧ P b) ∧ ownG m)%I).
+  * eapply pvs_ownG_updateP, iprod_singleton_updateP;
+      first (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
+    naive_solver.
+  * apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
+    rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
 Qed.
 
-Lemma pvs_update E γ a a' : a ~~> a' → own γ a ⊑ pvs E E (own γ a').
+Lemma pvs_update E γ a a' : a ~~> a' → own i γ a ⊑ pvs E E (own i γ a').
 Proof.
   intros; rewrite (pvs_updateP E _ _ (a' =)); last by apply cmra_update_updateP.
   by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
 Qed.
-
 End global.
diff --git a/program_logic/upred.v b/program_logic/upred.v
index 7bafefba9453dbddd20bda856ae98f69f170d1ed..12df00e7aeae21ab5ee77bf0ccab6b06c9611936 100644
--- a/program_logic/upred.v
+++ b/program_logic/upred.v
@@ -208,7 +208,7 @@ Arguments uPred_holds {_} _%I _ _.
 Arguments uPred_entails _ _%I _%I.
 Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
 Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
-Notation "■ φ" := (uPred_const φ) (at level 20) : uPred_scope.
+Notation "■ φ" := (uPred_const φ%type) (at level 20) : uPred_scope.
 Notation "'False'" := (uPred_const False) : uPred_scope.
 Notation "'True'" := (uPred_const True) : uPred_scope.
 Infix "∧" := uPred_and : uPred_scope.