diff --git a/theories/Dot/dotsyn.v b/theories/Dot/dotsyn.v
index c8c2b78a8..132975235 100644
--- a/theories/Dot/dotsyn.v
+++ b/theories/Dot/dotsyn.v
@@ -1,7 +1,7 @@
-From stdpp Require Import numbers.
+From stdpp Require Import numbers strings.
 From D Require Export prelude tactics.
 
-Definition label := nat.
+Definition label := string.
 
 Inductive tm  : Type :=
   | tv : vl -> tm
@@ -12,7 +12,7 @@ Inductive tm  : Type :=
   | var_vl : var -> vl
   | vnat : nat -> vl
   | vabs : tm -> vl
-  | vobj : (list dm) -> vl
+  | vobj : list (label * dm) -> vl
  with dm  : Type :=
   | dtysyn : ty -> dm
   | dtysem : (list vl) -> positive -> dm
@@ -35,13 +35,33 @@ Inductive tm  : Type :=
   | TNat :  ty.
 
 Definition vls := list vl.
-Definition dms := list dm.
+Definition dms := list (label * dm).
 Definition ctx := list ty.
 
 Implicit Types
          (T: ty) (v: vl) (t e: tm) (d: dm) (ds: dms) (vs: vls)
          (Γ : ctx).
 
+Definition label_of_ty (T: ty): option label :=
+  match T with
+  | TTMem l _ _ => Some l
+  | TVMem l _ => Some l
+  | _ => None
+  end.
+
+Fixpoint dms_lookup (l : label) (ds : dms): option dm :=
+  match ds with
+  | [] => None
+  | (l', d) :: ds =>
+    match (decide (l = l')) with
+    | left Heq => Some d
+    | right _ => dms_lookup l ds
+    end
+  end.
+
+Definition dms_has ds l d := dms_lookup l ds = Some d.
+Definition dms_hasnt ds l := dms_lookup l ds = None.
+
 (* Module Coq_IndPrinciples_Bad. *)
 (*   Scheme tm_bad_mut_ind := Induction for tm Sort Prop *)
 (*   with   vl_bad_mut_ind := Induction for vl Sort Prop *)
@@ -79,7 +99,7 @@ Section syntax_mut_rect.
   Variable step_vabs: ∀ t, Ptm t → Pvl (vabs t).
   (* Original: *)
   (* Variable step_vobj: ∀ l, Pvl (vobj l). *)
-  Variable step_vobj: ∀ ds, ForallT Pdm ds → Pvl (vobj ds).
+  Variable step_vobj: ∀ ds, ForallT Pdm (map snd ds) → Pvl (vobj ds).
   Variable step_dtysyn: ∀ T, Pty T → Pdm (dtysyn T).
   (* Original: *)
   (* Variable step_dtysem: ∀ vsl g, Pdm (dtysem vs g). *)
@@ -118,7 +138,8 @@ Section syntax_mut_rect.
       | Hstep: context [?P (?c _)] |- ?P (?c _) => apply Hstep; trivial
       | Hstep: context [?P (?c)] |- ?P (?c) => apply Hstep; trivial
       end.
-    all: elim: l => [|x xs IHxs] //=; auto.
+    - elim: l => [|[l d] ds IHds] //=; auto.
+    - elim: l => [|v vs IHxs] //=; auto.
   Qed.
 
   Lemma syntax_mut_rect: (∀ t, Ptm t) * (∀ v, Pvl v) * (∀ d, Pdm d) * (∀ p, Ppt p) * (∀ T, Pty T).
@@ -148,7 +169,7 @@ Section syntax_mut_ind.
   Variable step_vabs: ∀ t, Ptm t → Pvl (vabs t).
   (* Original: *)
   (* Variable step_vobj: ∀ l, Pvl (vobj l). *)
-  Variable step_vobj: ∀ ds, Forall Pdm ds → Pvl (vobj ds).
+  Variable step_vobj: ∀ ds, Forall Pdm (map snd ds) → Pvl (vobj ds).
   Variable step_dtysyn: ∀ T, Pty T → Pdm (dtysyn T).
   (* Original: *)
   (* Variable step_dtysem: ∀ vsl g, Pdm (dtysem vs g). *)
@@ -196,8 +217,12 @@ Instance Ids_vls : Ids vls := _.
 Instance Ids_dms : Ids dms := _.
 Instance Ids_ctx : Ids ctx := _.
 
+Definition mapsnd {A} `(f: B → C) : A * B → A * C := λ '(a, b), (a, f b).
+
 Instance list_rename `{Rename X} : Rename (list X) :=
   λ sb xs, map (rename sb) xs.
+Instance list_pair_rename {A} `{Rename X}: Rename (list (A * X)) :=
+  λ sb xs, map (mapsnd (rename sb)) xs.
 
 Fixpoint tm_rename (sb : var → var) (e : tm) {struct e} : tm :=
   let a := tm_rename : Rename tm in
@@ -262,17 +287,19 @@ Instance Rename_dm : Rename dm := dm_rename.
 Instance Rename_pth : Rename path := path_rename.
 
 Definition list_rename_fold `{Rename X} (sb : var → var) (xs : list X) : map (rename sb) xs = rename sb xs := eq_refl.
+Definition list_pair_rename_fold {A} `{Rename X} sb (xs: list (A * X)): map (mapsnd (rename sb)) xs = rename sb xs := eq_refl.
 
 Definition vls_rename_fold: ∀ sb vs, map (rename sb) vs = rename sb vs := list_rename_fold.
-Definition dms_rename_fold: ∀ sb ds, map (rename sb) ds = rename sb ds := list_rename_fold.
 Definition ctx_rename_fold: ∀ sb Γ, map (rename sb) Γ = rename sb Γ := list_rename_fold.
+Definition dms_rename_fold: ∀ sb ds, map (mapsnd (rename sb)) ds = rename sb ds := list_pair_rename_fold.
 
-Hint Rewrite @list_rename_fold : autosubst.
+Hint Rewrite @list_rename_fold @list_pair_rename_fold : autosubst.
 
 Instance vls_hsubst `{Subst vl} : HSubst vl vls :=
   λ (sb : var → vl) (vs : vls), map (subst sb) vs.
 
 Instance list_hsubst `{HSubst vl X}: HSubst vl (list X) := λ sb xs, map (hsubst sb) xs.
+Instance list_pair_hsubst {A} `{HSubst vl X}: HSubst vl (list (A * X)) := λ sb xs, map (mapsnd (hsubst sb)) xs.
 
 Fixpoint tm_hsubst (sb : var → vl) (e : tm) : tm :=
   let a := tm_hsubst : HSubst vl tm in
@@ -345,11 +372,13 @@ Hint Mode HSubst - + : typeclass_instances.
 
 Definition vls_subst_fold (sb : var → vl) (vs : vls) : map (subst sb) vs = hsubst sb vs := eq_refl.
 Definition list_hsubst_fold `{HSubst vl X} sb (xs : list X) : map (hsubst sb) xs = hsubst sb xs := eq_refl.
+Definition list_pair_hsubst_fold {A} `{HSubst vl X} sb (xs : list (A * X)) : map (mapsnd (hsubst sb)) xs = hsubst sb xs := eq_refl.
 
-Hint Rewrite vls_subst_fold @list_hsubst_fold : autosubst.
+Hint Rewrite vls_subst_fold @list_hsubst_fold @list_pair_hsubst_fold : autosubst.
 
 Arguments vls_hsubst /.
 Arguments list_hsubst /.
+Arguments list_pair_hsubst /.
 
 Lemma vl_eq_dec (v1 v2 : vl) : Decision (v1 = v2)
 with
@@ -362,9 +391,10 @@ with
 path_eq_dec (pth1 pth2 : path) : Decision (pth1 = pth2).
 Proof.
    all: rewrite /Decision; decide equality;
-       try (apply vl_eq_dec || apply tm_eq_dec || apply ty_eq_dec || apply path_eq_dec ||
+       try repeat (apply vl_eq_dec || apply tm_eq_dec || apply ty_eq_dec || apply path_eq_dec ||
+            apply @prod_eq_dec ||
             apply @list_eq_dec ||
-            apply nat_eq_dec || apply positive_eq_dec); auto.
+            apply nat_eq_dec || apply positive_eq_dec || apply string_eq_dec); auto.
 Qed.
 
 Instance vl_eq_dec' : EqDecision vl := vl_eq_dec.
@@ -376,7 +406,7 @@ Instance vls_eq_dec' : EqDecision vls := list_eq_dec.
 Instance dms_eq_dec' : EqDecision dms := list_eq_dec.
 
 Local Ltac finish_lists l x :=
-  elim: l => [|x xs IHds] //=; by f_equal.
+  elim: l => [|x xs IHds] //=; idtac + elim: x => [l d] //=; f_equal => //; by f_equal.
 
 Lemma vl_rename_Lemma (ξ : var → var) (v : vl) : rename ξ v = v.[ren ξ]
 with
@@ -493,9 +523,15 @@ Proof.
     induction s; asimpl; by f_equal.
 Qed.
 
-Instance HSubstLemmas_dms : HSubstLemmas vl dms := _.
 Instance HSubstLemmas_ctx : HSubstLemmas vl ctx := _.
 
+Instance HSubstLemmas_list_pair {A} `{Ids X} `{HSubst vl X} {hsl: HSubstLemmas vl X}: HSubstLemmas vl (list (A * X)).
+Proof.
+  split; trivial; intros; rewrite /hsubst /list_pair_hsubst;
+    elim: s => [|[l d] xs IHds] //; asimpl; by f_equal.
+Qed.
+Instance HSubstLemmas_dms : HSubstLemmas vl dms := _.
+
 (** After instantiating Autosubst, a few binding-related syntactic definitions
     that need not their own file. *)
 
@@ -557,6 +593,9 @@ Ltac solve_fv_congruence :=
 Lemma fv_cons `{Ids X} `{HSubst vl X} {hsla: HSubstLemmas vl X} (x: X) xs n: nclosed xs n → nclosed x n → nclosed (x :: xs) n.
 Proof. solve_fv_congruence. Qed.
 
+Lemma fv_pair_cons {A} `{Ids X} `{HSubst vl X} {hsla: HSubstLemmas vl X} (a: A) (x: X) xs n: nclosed xs n → nclosed x n → nclosed ((a, x) :: xs) n.
+Proof. solve_fv_congruence. Qed.
+
 (** The following ones are "inverse" lemmas: by knowing that an expression is closed,
     deduce that one of its subexpressions is closed *)
 
diff --git a/theories/Dot/fundamental.v b/theories/Dot/fundamental.v
index dede713a3..cf26e8660 100644
--- a/theories/Dot/fundamental.v
+++ b/theories/Dot/fundamental.v
@@ -44,9 +44,9 @@ Section fundamental.
     iIntros "#H".
     cbn; fold t_dm t_dms.
     (* remember t_dms as t_ds eqn:Heqt. unfold t_dms in Heqt. rewrite -Heqt. fold t_dms in Heqt. rewrite Heqt. *)
-    iInduction ds as [] "IHds" forall (ds'); destruct ds' => //.
+    iInduction ds as [|(l, d) ds] "IHds" forall (ds'); destruct ds' as [| (l', d') ds' ]=> //.
                                       cbn; fold t_dms.
-                                      iDestruct "H" as "[Hd Hds]".
+                                      iDestruct "H" as "[% [Hd Hds]]".
                                         by iPoseProof ("IHds" with "Hds") as "<-".
   Qed.
 
@@ -61,9 +61,9 @@ Section fundamental.
     iIntros (Hlook1 Hlook2) "#HTr".
     inversion Hlook1 as (ds1 & -> & Hl1).
     inversion Hlook2 as (ds2 & -> & Hl2).
-    rewrite lookup_reverse_indexr in Hl1.
-    rewrite lookup_reverse_indexr in Hl2.
-    iInduction ds1 as [| dh1 ds1] "IHds" forall (ds2 Hlook2 Hl2); destruct ds2 as [|dh2 ds2]=>//.
+    (* rewrite lookup_reverse_indexr in Hl1. *)
+    (* rewrite lookup_reverse_indexr in Hl2. *)
+    iInduction ds1 as [| (l1, dh1) ds1] "IHds" forall (ds2 Hlook2 Hl2); destruct ds2 as [|(l2, dh2) ds2]=>//.
     iPoseProof (transl_len with "HTr") as "%". move: H => Hlen.
     injection Hlen; clear Hlen; intro Hlen.
     cbn in *; fold t_dm t_dms.
@@ -84,14 +84,15 @@ Section fundamental.
     destruct v => //.
     iPoseProof (transl_len with "HTr1") as "%". move: H => Hlen1.
     iPoseProof (transl_len with "HTr2") as "%". move: H => Hlen2.
-    assert (∃ d, reverse (selfSubst l0) !! l = Some d) as [d Hl]. {
-      apply lookup_lt_is_Some_2.
-      rewrite reverse_length selfSubst_len Hlen1 -selfSubst_len -reverse_length.
-      eapply lookup_lt_is_Some_1. rewrite Hl1; eauto.
+    assert (∃ d, dms_lookup l (selfSubst l0) = Some d) as [d Hl]. {
+      (* (* apply lookup_lt_is_Some_2. *) *)
+      (* rewrite reverse_length selfSubst_len Hlen1 -selfSubst_len -reverse_length. *)
+      (* eapply lookup_lt_is_Some_1. rewrite Hl1; eauto. *)
+      admit.
     }
     assert (vobj l0 @ l ↘ d). by exists l0.
     iExists d. repeat iSplit => //; by iApply transl_lookup_commute'.
-  Qed.
+  Admitted.
 
   Lemma lookups_agree v0 v1 v2 ρ σ1 σ2 γ1 γ2 φ1  l:
     v1.[to_subst ρ] @ l ↘ dtysem σ1 γ1 → v2.[to_subst ρ] @ l ↘ dtysem σ2 γ2 →
diff --git a/theories/Dot/lr_lemmasDefs.v b/theories/Dot/lr_lemmasDefs.v
index 13fc1b143..ca86bc2ca 100644
--- a/theories/Dot/lr_lemmasDefs.v
+++ b/theories/Dot/lr_lemmasDefs.v
@@ -14,7 +14,7 @@ Section Sec.
      worst-case, we can add a fancy update to definition typing. *)
   Lemma idtp_vmem_i T v l:
     ivtp Γ (TLater T) v -∗
-    Γ ⊨d { l = dvl v } : TVMem l T.
+    Γ ⊨d dvl v : TVMem l T.
   Proof.
     iIntros "#[% #Hv]". move: H => Hclv. iSplit. auto using fv_dvl. iIntros "!> * #Hg".
     iPoseProof (interp_env_ρ_closed with "Hg") as "%". move: H => Hclρ.
@@ -63,7 +63,7 @@ Section Sec.
     Γ ⊨ [T, 1] <: [U, 1] -∗
     Γ ⊨ [L, 1] <: [T, 1] -∗
     γ ⤇ dot_interp T -∗
-    Γ ⊨d { l = dtysem (idsσ (length Γ)) γ } : TTMem l L U.
+    Γ ⊨d dtysem (idsσ (length Γ)) γ : TTMem l L U.
   Proof.
     iIntros " #HLU #HTU #HLT #Hγ /=".
     iSplit. by auto using fv_dtysem, fv_idsσ.
@@ -100,51 +100,58 @@ Section Sec.
 
   Lemma idtp_tmem_i T γ l:
     γ ⤇ dot_interp T -∗
-    Γ ⊨d { l = dtysem (idsσ (length Γ)) γ } : TTMem l T T.
+    Γ ⊨d dtysem (idsσ (length Γ)) γ : TTMem l T T.
   Proof.
     iIntros " #Hγ".
     iApply (idtp_tmem_abs_i T T T) => //=;
       by iIntros "!> **".
   Qed.
 
-  Lemma dtp_tand_i T U ρ d ds:
-    defs_interp T ρ ds -∗
-    def_interp U (length ds) ρ d -∗
-    defs_interp (TAnd T U) ρ (cons d ds).
-  Proof. naive_solver. Qed.
+  (* Lemma dtp_tand_i T U ρ d ds l: *)
+  (*   defs_interp T ρ ds -∗ *)
+  (*   def_interp U ρ d -∗ *)
+  (*   defs_interp (TAnd T U) ρ (cons (l, d) ds). *)
+  (* Proof. naive_solver. Qed. *)
 
-  Lemma def_interp_to_interp T d ds ρ s:
-    let v0 := (vobj (d :: ds)).[s] in
+  Lemma def_interp_to_interp T d ds ρ s l:
+    let v0 := (vobj ((l, d) :: ds)).[s] in
     nclosed_vl v0 0 →
-    def_interp T (length ds) ρ (d.|[v0 .: s]) ⊢
+    label_of_ty T = Some l →
+    def_interp T ρ (d.|[v0 .: s]) ⊢
     interp T ρ v0.
   Proof.
-    intros * Hfvv0. asimpl.
+    intros * Hfvv0 HTlabel. asimpl.
     set (d' := d.|[up s]); set (ds' := ds.|[up s]).
-    assert (nclosed_vl (vobj (d' :: ds')) 0) as Hfv'. {
+    assert (nclosed_vl (vobj ((l, d') :: ds')) 0) as Hfv'. {
       revert v0 Hfvv0.
       asimpl.
       by subst d' ds'.
     }
     assert (length ds = length ds') as Hlen'. by rewrite /ds' /hsubst map_length.
-    assert (vobj (d' :: ds') @ length ds ↘ d'.|[vobj (d' :: ds')/]) as Hlookup.
-      by rewrite Hlen'; apply obj_lookup_cons.
+    assert (vobj ((l, d') :: ds') @ l ↘ d'.|[vobj ((l, d') :: ds')/]) as Hlookup.
+    admit.
+      (* XXX we need to rewrite this lemma for the new lookup relation, after fixing typing.
+        by rewrite Hlen'; apply obj_lookup_cons. *)
     induction T => //=; try (by iIntros "**").
-    all: iIntros "[% [% #H]]"; move: H H0 => Hlen Hfvd; rewrite <- Hlen.
+    all: cbn in HTlabel; injectHyps; iIntros "[% #H]"; move: H => Hvd.
     - iDestruct "H" as (vmem) "[#H1 #H2]".
       iSplit => //.
-      iExists (d'.|[vobj (d' :: ds')/]). iSplit => //.
-      subst d'. asimpl.
+      iExists (d'.|[vobj ((l, d') :: ds')/]).
+      subst d' ds'; iSplit => //.
+      asimpl; trivial.
+      (* subst d' ds'. asimpl. apply Hlookup. *)
+      (* subst; eauto. *)
+      (* subst d'. asimpl. *)
       iSplit => //. iExists _. iSplit => //.
     - iDestruct "H" as (φ σ) "[#Hl [#? [#? #?]]]".
       iDestruct "Hl" as (γ) "[% #Hγ]". move: H => Hl.
       iSplit => //.
-      iExists (d'.|[vobj (d' :: ds')/]). iSplit => //.
+      iExists (d'.|[vobj ((l, d') :: ds')/]). iSplit => //.
       subst d'; asimpl.
       iSplit => //. iExists φ, σ; iSplit => //.
       * iExists γ; iSplit => //.
       * iModIntro. repeat iSplitL; naive_solver.
-  Qed.
+  Admitted.
 
   (* Formerly wip_hard. *)
   Lemma defs_interp_to_interp T ds ρ s:
@@ -163,32 +170,33 @@ Section Sec.
 
     simpl; iIntros (Hcl) "#H".
     iPoseProof (defs_interp_v_closed with "H") as "%". move: H => Hclds.
-    iInduction T as [] "IHT" forall (ds Hcl Hclds) => //.
-    destruct ds => //=. rewrite map_length.
-    iDestruct "H" as "[#H1 #H2]".
-    iSplit.
-    2: { by iApply (def_interp_to_interp T2 d ds ρ s). }
-    - asimpl.
-      iAssert (⟦ T1 ⟧ ρ (vobj (ds.|[up s]))) as "#H3". {
-        iApply ("IHT" $! ds) => //.
-        admit.
-        admit.
-        asimpl.
-        Fail iApply "H1".
-        admit.
-      }
-      (* We could probably go from H3 to the thesis... *)
-      iApply ("IHT" $! (d :: ds)) => //.
-      admit.
-
-      (* iApply (IHT1 (d :: ds)). *)
-      (* set (d' := d.|[up (to_subst ρ)]). *)
-      (* set (ds' := ds.|[up (to_subst ρ)]). *)
-      (* change (ds.|[up (to_subst ρ)]) with ds'. *)
-
-    (* simpl. *)
-    (* induction T; rewrite /defs_interp => //=; fold defs_interp; *)
-    (* try solve [iIntros; try done]. *)
+    iInduction T as [] "IHT" forall (ds Hcl Hclds) => //=; try iDestruct "H" as (l1 d) "[% H']"; trivial.
+
+    (* destruct ds => //=. rewrite map_length. *)
+    (* iDestruct "H" as "[#H1 #H2]". *)
+    (* iSplit. *)
+    (* 2: { by iApply (def_interp_to_interp T2 d ds ρ s). } *)
+    (* - asimpl. *)
+    (*   iAssert (⟦ T1 ⟧ ρ (vobj (ds.|[up s]))) as "#H3". { *)
+    (*     iApply ("IHT" $! ds) => //. *)
+    (*     admit. *)
+    (*     admit. *)
+    (*     asimpl. *)
+    (*     Fail iApply "H1". *)
+    (*     admit. *)
+    (*   } *)
+    (*   (* We could probably go from H3 to the thesis... *) *)
+    (*   iApply ("IHT" $! (d :: ds)) => //. *)
+    (*   admit. *)
+
+    (*   (* iApply (IHT1 (d :: ds)). *) *)
+    (*   (* set (d' := d.|[up (to_subst ρ)]). *) *)
+    (*   (* set (ds' := ds.|[up (to_subst ρ)]). *) *)
+    (*   (* change (ds.|[up (to_subst ρ)]) with ds'. *) *)
+
+    (* (* simpl. *) *)
+    (* (* induction T; rewrite /defs_interp => //=; fold defs_interp; *) *)
+    (* (* try solve [iIntros; try done]. *) *)
   Admitted.
 
   (* Check that Löb induction works as expected for proving introduction of
diff --git a/theories/Dot/operational.v b/theories/Dot/operational.v
index fc3e8db0d..4e2096500 100644
--- a/theories/Dot/operational.v
+++ b/theories/Dot/operational.v
@@ -84,12 +84,21 @@ Qed.
 
 End saved_interp.
 
+Implicit Types
+         (T: ty) (v: vl) (t e: tm) (d: dm) (ds: dms) (vs: vls)
+         (Γ : ctx).
 (** Substitute object inside itself (to give semantics to the "self"
     variable). To use when descending under the [vobj] binder. *)
-Definition selfSubst (ds: dms): dms := ds.|[vobj ds/].
+Definition selfSubst ds: dms := ds.|[vobj ds/].
 
-Definition objLookup v l d: Prop :=
-  ∃ ds, v = vobj ds ∧ reverse (selfSubst ds) !! l = Some d.
+(* Unset Program Cases. *)
+(* Definition gmap_of_dms ds: gmap label dm := map_of_list ds. *)
+(* Definition dms_lookup l ds := gmap_of_dms ds !! l. *)
+(* Arguments gmap_of_dms /. *)
+(* Arguments dms_lookup /. *)
+
+Definition objLookup v (l: label) d: Prop :=
+  ∃ ds, v = vobj ds ∧ (dms_lookup l (selfSubst ds)) = Some d.
 Notation "v @ l ↘ d" := (objLookup v l d) (at level 20).
 
 (** Instead of letting obj_opens_to autounfold,
@@ -113,98 +122,116 @@ Ltac objLookupDet :=
     assert (d2 = d1) as ? by (eapply objLookupDet; eassumption); injectHyps
   end.
 
-Section AboutObjLookup.
+(* Section AboutObjLookup. *)
 (** Auxiliary definitions to prove [lookup_reverse_length], since a direct inductive proof appers to fail (but
 see rev_append_map for an approach that has a chance). *)
-Fixpoint indexr {X} (i: nat) (xs: list X) : option X :=
-  match xs with
-  | [] => None
-  | x :: xs =>
-    if decide (i = length xs) then Some x else indexr i xs
-  end.
-
-Lemma indexr_max {X} (T: X) i vs:
-                       indexr i vs = Some T ->
-                       i < length vs.
-Proof.
-  induction vs; first done; rewrite /lt in IHvs |- *; move => /= H.
-  case_decide; subst; [ lia | eauto ].
-Qed.
-Hint Resolve indexr_max.
-
-Lemma lookup_reverse_indexr {X} (ds: list X) l: reverse ds !! l = indexr l ds.
-Proof.
-  elim: ds l => [|d ds IHds] l //=.
-  case_decide; subst.
-  - by rewrite reverse_cons lookup_app_r reverse_length ?Nat.sub_diag.
-  - case (decide (l < length ds)) => Hl.
-    + by rewrite reverse_cons lookup_app_l ?reverse_length.
-    + assert (l > length ds) by omega.
-      assert (indexr l ds = None). {
-        destruct (indexr l ds) eqn:? => //.
-        assert (l < length ds) by (eapply indexr_max; eauto).
-        lia.
-      }
-      by rewrite lookup_ge_None_2 ?reverse_length.
-Qed.
-
-Lemma lookup_reverse_length {X} l (d: X) ds: l = length ds → reverse (d :: ds) !! l = Some d.
-Proof.
-  intros; subst. rewrite lookup_reverse_indexr /=. case_decide => //=.
-Qed.
+(* Fixpoint indexr {X} (i: nat) (xs: list X) : option X := *)
+(*   match xs with *)
+(*   | [] => None *)
+(*   | x :: xs => *)
+(*     if decide (i = length xs) then Some x else indexr i xs *)
+(*   end. *)
+
+(* Lemma indexr_max {X} (x: X) i xs: *)
+(*                        indexr i xs = Some x -> *)
+(*                        i < length xs. *)
+(* Proof. *)
+(*   induction xs; first done; rewrite /lt in IHxs |- *; move => /= H. *)
+(*   case_decide; subst; [ lia | eauto ]. *)
+(* Qed. *)
+(* Hint Resolve indexr_max. *)
 
-Lemma obj_lookup_cons d ds: vobj (d :: ds) @ length ds ↘ d.|[vobj (d :: ds)/].
-Proof.
-  hnf. eexists; split; trivial.
-  rewrite /selfSubst /=. apply lookup_reverse_length. by rewrite map_length.
-Qed.
+(* Lemma lookup_reverse_indexr {X} (ds: list X) l: reverse ds !! l = indexr l ds. *)
+(* Proof. *)
+(*   elim: ds l => [|d ds IHds] l //=. *)
+(*   case_decide; subst. *)
+(*   - by rewrite reverse_cons lookup_app_r reverse_length ?Nat.sub_diag. *)
+(*   - case (decide (l < length ds)) => Hl. *)
+(*     + by rewrite reverse_cons lookup_app_l ?reverse_length. *)
+(*     + assert (l > length ds) by omega. *)
+(*       assert (indexr l ds = None). { *)
+(*         destruct (indexr l ds) eqn:? => //. *)
+(*         assert (l < length ds) by (eapply indexr_max; eauto). *)
+(*         lia. *)
+(*       } *)
+(*       by rewrite lookup_ge_None_2 ?reverse_length. *)
+(* Qed. *)
 
-Lemma indexr_extend {X} vs n x (T: X):
-                       indexr n vs = Some T ->
-                       indexr n (x::vs) = Some T.
-Proof.
-  move => H /=; assert (n < length vs) by naive_solver; by case_decide; first lia.
-Qed.
-Hint Resolve indexr_extend.
+(* Lemma lookup_reverse_length {X} l (x: X) xs: l = length xs → reverse (x :: xs) !! l = Some x. *)
+(* Proof. *)
+(*   intros; subst. rewrite lookup_reverse_indexr /=. case_decide => //=. *)
+(* Qed. *)
 
-Lemma lookup_reverse_extend {X} l (d: X) ds:
-  reverse ds !! l = Some d →
-  reverse (d :: ds) !! l = Some d.
-Proof.
-  intros; subst. rewrite -> lookup_reverse_indexr in *. by apply indexr_extend.
-Qed.
+(* Lemma obj_lookup_cons d ds l: (l, d) ∈ ds → vobj ds @ l ↘ d.|[vobj ds/]. *)
+(* Proof. *)
+(*   hnf; move => Hin; eexists; split => //=. *)
+(*   elim: ds Hin => [|[l' d'] ds IHds] //= Hin; first inversion Hin. *)
+(*   (* destruct (decide (l = l')) as [-> | Hne]. *) *)
+(*   inverse Hin; rewrite ?lookup_insert /mapsnd //=. *)
+(*   apply IHds in H1. *)
+(*   destruct (decide (l = l')) as [Heq | Hne]. *)
+(*   admit. *)
+(*   cbn. *)
+(*   asimpl. cbn. *)
+(*   f_equal. *)
+(*   rewrite /selfSubst /=. *)
+  
+(*   assert ((l, d.|[vobj ds/]) ∈ ds.|[vobj ds/]). *)
+(*   rewrite /hsubst /list_pair_hsubst -/mapsnd. *)
+(*   set (sb := (hsubst (vobj ds .: ids))). *)
+(*   assert (map (mapsnd ) (l, d.|[vobj ds/]) ∈ ds.|[vobj ds/]). *)
+  
+(*   Search "_ ∈ _". *)
+(*   assert ((l, d) ∈ gmap_of_dms ds). *)
+(*   apply lookup_reverse_length. by rewrite map_length. *)
+(* Qed. *)
 
-Lemma rev_append_map {X Y} (xs1 xs2: list X) (f: X → Y): rev_append (map f xs1) (map f xs2) = map f (rev_append xs1 xs2).
-Proof.
-  elim: xs1 xs2 => [|x xs1 IH] xs2 //=. eapply (IH (x :: xs2)).
-Qed.
-Lemma reverse_map {X Y} (xs: list X) (f: X → Y): reverse (map f xs) = map f (reverse xs).
-Proof. rewrite /reverse. eapply (rev_append_map xs []). Qed.
+(* Lemma indexr_extend {X} vs n x (T: X): *)
+(*                        indexr n vs = Some T -> *)
+(*                        indexr n (x::vs) = Some T. *)
+(* Proof. *)
+(*   move => H /=; assert (n < length vs) by naive_solver; by case_decide; first lia. *)
+(* Qed. *)
+(* Hint Resolve indexr_extend. *)
 
-Lemma lookup_map {X Y} x (xs: list X) (f: X → Y) l: xs !! l = Some x → map f xs !! l = Some (f x).
-Proof.
-  elim: xs l => /= [|x' xs IH] [|l] //= Hl; by [cinject Hl | apply IH].
-Qed.
+(* Lemma lookup_reverse_extend {X} l (d: X) ds: *)
+(*   reverse ds !! l = Some d → *)
+(*   reverse (d :: ds) !! l = Some d. *)
+(* Proof. *)
+(*   intros; subst. rewrite -> lookup_reverse_indexr in *. by apply indexr_extend. *)
+(* Qed. *)
 
-(* Lemma lookup_map_inv {X Y} x (xs: list X) (f: X → Y) l: map f xs !! l = Some (f x) → xs !! l = Some x. *)
+(* Lemma rev_append_map {X Y} (xs1 xs2: list X) (f: X → Y): rev_append (map f xs1) (map f xs2) = map f (rev_append xs1 xs2). *)
 (* Proof. *)
-(*   elim: xs l => [|x' xs IH] [|l] //=. (* ONLY FOR F INDUCTIVE! *) *)
+(*   elim: xs1 xs2 => [|x xs1 IH] xs2 //=. eapply (IH (x :: xs2)). *)
+(* Qed. *)
+(* Lemma reverse_map {X Y} (xs: list X) (f: X → Y): reverse (map f xs) = map f (reverse xs). *)
+(* Proof. rewrite /reverse. eapply (rev_append_map xs []). Qed. *)
 
-(* Lemma obj_lookup_extend d ds l: *)
-(*   vobj ds @ l ↘ d.|[vobj ds/] → *)
-(*   vobj (d :: ds) @ l ↘ d.|[vobj (d :: ds)/]. *)
+(* Lemma lookup_map {X Y} x (xs: list X) (f: X → Y) l: xs !! l = Some x → map f xs !! l = Some (f x). *)
 (* Proof. *)
-(*   hnf. *)
-(*   intros (ds0 & Heq & Hl). cinject Heq. *)
-(*   eexists; split; trivial. *)
-(*   move: Hl. rewrite /selfSubst /lookup_reverse_indexr /= => Hl. *)
-(*   apply lookup_reverse_extend. *)
-(*   move: Hl. rewrite /hsubst /HSubst_dm !reverse_map => Hl. *)
-(*   apply lookup_map. apply lookup_map_inv in Hl. apply Hl. *)
-(*   (* eauto using lookup_map, lookup_map_inv. *) *)
+(*   elim: xs l => /= [|x' xs IH] [|l] //= Hl; by [cinject Hl | apply IH]. *)
 (* Qed. *)
 
-End AboutObjLookup.
+(* (* Lemma lookup_map_inv {X Y} x (xs: list X) (f: X → Y) l: map f xs !! l = Some (f x) → xs !! l = Some x. *) *)
+(* (* Proof. *) *)
+(* (*   elim: xs l => [|x' xs IH] [|l] //=. (* ONLY FOR F INDUCTIVE! *) *) *)
+
+(* (* Lemma obj_lookup_extend d ds l: *) *)
+(* (*   vobj ds @ l ↘ d.|[vobj ds/] → *) *)
+(* (*   vobj (d :: ds) @ l ↘ d.|[vobj (d :: ds)/]. *) *)
+(* (* Proof. *) *)
+(* (*   hnf. *) *)
+(* (*   intros (ds0 & Heq & Hl). cinject Heq. *) *)
+(* (*   eexists; split; trivial. *) *)
+(* (*   move: Hl. rewrite /selfSubst /lookup_reverse_indexr /= => Hl. *) *)
+(* (*   apply lookup_reverse_extend. *) *)
+(* (*   move: Hl. rewrite /hsubst /HSubst_dm !reverse_map => Hl. *) *)
+(* (*   apply lookup_map. apply lookup_map_inv in Hl. apply Hl. *) *)
+(* (*   (* eauto using lookup_map, lookup_map_inv. *) *) *)
+(* (* Qed. *) *)
+
+(* End AboutObjLookup. *)
 
 (** Instantiating iris with  *)
 Module lang.
@@ -236,7 +263,7 @@ Inductive head_step : tm -> state -> list observation -> tm -> state -> list tm
 | st_beta t1 v2 σ:
     head_step (tapp (tv (vabs t1)) (tv v2)) σ [] (t1.|[v2/]) σ []
 | st_proj ds l σ v:
-    reverse (selfSubst ds) !! l = Some (dvl v) ->
+    dms_lookup l (selfSubst ds) = Some (dvl v) ->
     head_step (tproj (tv (vobj ds)) l) σ [] (tv v) σ []
 | st_skip t σ:
     head_step (tskip t) σ [] t σ [].
diff --git a/theories/Dot/rules.v b/theories/Dot/rules.v
index a778c44b3..8b90951a8 100644
--- a/theories/Dot/rules.v
+++ b/theories/Dot/rules.v
@@ -33,7 +33,7 @@ Section lang_rules.
   Proof. solve_pure_exec. Qed.
 
   Global Instance pure_tproj ds l v :
-    PureExec (reverse (selfSubst ds) !! l = Some (dvl v)) 1 (tproj (tv (vobj ds)) l) (tv v).
+    PureExec (dms_lookup l (selfSubst ds) = Some (dvl v)) 1 (tproj (tv (vobj ds)) l) (tv v).
   Proof. solve_pure_exec. Qed.
 
   Global Instance pure_tskip t:
diff --git a/theories/Dot/skeleton.v b/theories/Dot/skeleton.v
index 7c06d3a8c..b7d91659b 100644
--- a/theories/Dot/skeleton.v
+++ b/theories/Dot/skeleton.v
@@ -23,8 +23,8 @@ same_skel_vl (v1 v2: vl): Prop :=
     let fix same_skel_dms (ds1 ds2: dms): Prop :=
         match (ds1, ds2) with
         | (nil, nil) => True
-        | (cons d1 ds1, cons d2 ds2) =>
-          same_skel_dm d1 d2 ∧ same_skel_dms ds1 ds2
+        | (cons (l1, d1) ds1, cons (l2, d2) ds2) =>
+          l1 = l2 ∧ same_skel_dm d1 d2 ∧ same_skel_dms ds1 ds2
         | _ => False
         end
     in same_skel_dms ds1 ds2
@@ -111,12 +111,14 @@ Proof.
     cbn in Hske |- *; try inversion Hske; ev; asimpl; auto using same_skel_vl_subst.
   Qed.
 
-Definition same_skel_dms (ds1 ds2: dms): Prop := Forall2 same_skel_dm ds1 ds2.
+(* Maybe copy-paste instead same_skel_dms from above. Or switch everything to an inductive definition, *)
+Definition same_skel_dms (ds1 ds2: dms): Prop :=
+  Forall2 (λ '(l1, d1) '(l2, d2), l1 = l2 ∧ same_skel_dm d1 d2) ds1 ds2.
 
 Lemma same_skel_dms_index ds ds' v l:
   same_skel_dms ds ds' →
-  reverse (selfSubst ds) !! l = Some (dvl v) →
-  exists v', reverse (selfSubst ds') !! l = Some (dvl v') ∧ same_skel_vl v v'.
+  dms_lookup l (selfSubst ds) = Some (dvl v) →
+  exists v', dms_lookup l (selfSubst ds') = Some (dvl v') ∧ same_skel_vl v v'.
 Proof.
 Admitted.
 
diff --git a/theories/Dot/step_fv.v b/theories/Dot/step_fv.v
index 61529a935..eaf59ff29 100644
--- a/theories/Dot/step_fv.v
+++ b/theories/Dot/step_fv.v
@@ -26,31 +26,34 @@ Section nclosed_prim_step.
     nclosed ds (S n) → nclosed (selfSubst ds) n.
   Proof. move => Hcl. by apply nclosed_subst, fv_vobj. Qed.
 
-  Lemma fv_head d ds n: nclosed (d :: ds) n → nclosed d n.
+  Lemma fv_head l d ds n: nclosed ((l, d) :: ds) n → nclosed d n.
   Proof. solve_inv_fv_congruence. Qed.
   Hint Resolve fv_head: fvl.
 
-  Lemma fv_tail d ds n: nclosed (d :: ds) n → nclosed ds n.
+  Lemma fv_tail l d ds n: nclosed ((l, d) :: ds) n → nclosed ds n.
   Proof. solve_inv_fv_congruence. Qed.
   Hint Resolve fv_tail: fvl.
   Hint Resolve fv_dms_cons: fvl.
 
-  Lemma nclosed_rev_append (ds1 ds2: dms) n: nclosed ds1 n → nclosed ds2 n → nclosed (rev_append ds1 ds2) n.
-  Proof.
-    elim: ds1 ds2 => [|d1 ds1 IHds1] //= ds2 Hcl1 Hcl2.
-    assert (Hcld1: nclosed d1 n) by eauto with fvl.
-    assert (Hclds1: nclosed ds1 n) by eauto with fvl.
-    by apply IHds1, fv_dms_cons.
-  Qed.
+  (* Lemma nclosed_rev_append (ds1 ds2: dms) n: nclosed ds1 n → nclosed ds2 n → nclosed (rev_append ds1 ds2) n. *)
+  (* Proof. *)
+  (*   elim: ds1 ds2 => [|d1 ds1 IHds1] //= ds2 Hcl1 Hcl2. *)
+  (*   assert (Hcld1: nclosed d1 n) by eauto with fvl. *)
+  (*   assert (Hclds1: nclosed ds1 n) by eauto with fvl. *)
+  (*   by apply IHds1, fv_dms_cons. *)
+  (* Qed. *)
 
-  Lemma nclosed_reverse ds n: nclosed ds n → nclosed (reverse ds) n.
-  Proof. move => Hcl. by apply nclosed_rev_append. Qed.
+  (* Lemma nclosed_reverse ds n: nclosed ds n → nclosed (reverse ds) n. *)
+  (* Proof. move => Hcl. by apply nclosed_rev_append. Qed. *)
 
-  Lemma nclosed_lookup ds d n l: nclosed ds n → ds !! l = Some d → nclosed d n.
-  Proof. elim: ds l => [|d' ds IHds] [|l] //= Hcl Heq; simplify_eq; eauto with fvl. Qed.
+  Lemma nclosed_lookup ds d n l: nclosed ds n → dms_lookup l ds = Some d → nclosed d n.
+  Proof.
+    elim: ds => [|[l' d'] ds IHds] Hcl //= Heq.
+    case_decide; simplify_eq; eauto with fvl.
+  Qed.
 
   Lemma nclosed_proj ds l v n:
-    reverse (selfSubst ds) !! l = Some (dvl v) →
+    dms_lookup l (selfSubst ds) = Some (dvl v) →
     nclosed (tproj (tv (vobj ds)) l) n →
     nclosed (tv v) n.
   Proof.
@@ -58,7 +61,7 @@ Section nclosed_prim_step.
     assert (Hclt1: nclosed ds (S n)) by eauto with fv.
     apply fv_tv.
     enough (nclosed (dvl v) n) by eauto with fv.
-    eapply nclosed_lookup => //. by eapply nclosed_reverse, nclosed_selfSubst.
+    eapply nclosed_lookup => //. by eapply nclosed_selfSubst.
   Qed.
 
   Theorem nclosed_head_step t1 t2 σ σ' ts n:
diff --git a/theories/Dot/synLemmas.v b/theories/Dot/synLemmas.v
index acfd89119..50106aef9 100644
--- a/theories/Dot/synLemmas.v
+++ b/theories/Dot/synLemmas.v
@@ -180,7 +180,7 @@ Proof. solve_fv_congruence. Qed.
 Lemma fv_dtysem ρ γ l: nclosed ρ l → nclosed (dtysem ρ γ) l.
 Proof. solve_fv_congruence. Qed.
 
-Definition fv_dms_cons : ∀ d ds n, nclosed ds n → nclosed d n → nclosed (d :: ds) n := fv_cons.
+Definition fv_dms_cons : ∀ l d ds n, nclosed ds n → nclosed d n → nclosed ((l, d) :: ds) n := fv_pair_cons.
 
 Lemma fv_vls_cons v vs n: nclosed vs n → nclosed_vl v n → nclosed (v :: vs) n.
 Proof. solve_fv_congruence. Qed.
@@ -225,7 +225,7 @@ Proof.
 Qed.
 
 (* The proof of this lemma needs asimpl and hence is expensive. *)
-Lemma fv_vobj_ds_inv d ds n: nclosed_vl (vobj (d :: ds)) n → nclosed_vl (vobj ds) n.
+Lemma fv_vobj_ds_inv l d ds n: nclosed_vl (vobj ((l, d) :: ds)) n → nclosed_vl (vobj ds) n.
 Proof. solve_inv_fv_congruence. Qed.
 
 Lemma fv_tv_inv v n: nclosed (tv v) n → nclosed_vl v n.
diff --git a/theories/Dot/synToSem.v b/theories/Dot/synToSem.v
index c2d55f0c4..1abca21f7 100644
--- a/theories/Dot/synToSem.v
+++ b/theories/Dot/synToSem.v
@@ -99,8 +99,8 @@ Section Sec.
           (* ([∗ list] d1 ; d2 ∈ ds1 ; ds2 , t_dm d1 d2)%I *)
           match (ds1, ds2) with
           | (nil, nil) => True
-          | (cons d1 ds1, cons d2 ds2) =>
-            t_dm d1 d2 ∧ t_dms ds1 ds2
+          | (cons (l1, d1) ds1, cons (l2, d2) ds2) =>
+            ⌜l1 = l2⌝ ∧ t_dm d1 d2 ∧ t_dms ds1 ds2
           | _ => False
           end%I
       in
@@ -153,8 +153,8 @@ Section Sec.
     fix t_dms (ds1 ds2: dms) : iProp Σ :=
       match (ds1, ds2) with
       | (nil, nil) => True
-      | (cons d1 ds1, cons d2 ds2) =>
-        t_dm d1 d2 ∧ t_dms ds1 ds2
+      | (cons (l1, d1) ds1, cons (l2, d2) ds2) =>
+        ⌜l1 = l2⌝ ∧ t_dm d1 d2 ∧ t_dms ds1 ds2
       | _ => False
       end%I.
   Global Arguments t_dms _ /.
@@ -177,8 +177,9 @@ Section Sec.
   with  t_tm_persistent t1 t2: Persistent (t_tm t1 t2)
   with  t_dm_persistent t1 t2: Persistent (t_dm t1 t2).
   Proof.
-    all: revert t1 t2; induction t1; destruct t2;
-      try (revert l0; induction l; destruct l0);
+    all:
+      revert t1 t2; induction t1; destruct t2;
+      try (elim: l l0 => [|[l1 d1] ds1 IHds1] [|[l2 d2] ds2]);
       simpl; try apply _.
   Qed.
   Global Existing Instance t_ty_persistent.
@@ -189,8 +190,7 @@ Section Sec.
 
   Lemma t_dms_persistent ds1 ds2: Persistent (t_dms ds1 ds2).
   Proof.
-    revert ds1 ds2; induction ds1; destruct ds2; simpl;
-      try apply _.
+    elim: ds1 ds2 => [|[l1 d1] ds1 IHds1] [|[l2 d2] ds2] /=; try apply _.
   Qed.
   Global Existing Instance t_dms_persistent.
 
@@ -231,7 +231,7 @@ Section Sec.
       let fix is_syn_dms (ds: dms): Prop :=
           match ds with
           | nil => True
-          | cons d ds =>
+          | cons (l, d) ds =>
             is_syn_dm d ∧ is_syn_dms ds
           end
         in
@@ -279,7 +279,7 @@ Section Sec.
     fix is_syn_dms (ds: dms): Prop :=
       match ds with
       | nil => True
-      | cons d ds =>
+      | cons (l, d) ds =>
         is_syn_dm d ∧ is_syn_dms ds
       end.
 
@@ -387,9 +387,9 @@ Section Sec.
       try (iDestruct "Hyp2" as "[Hyp21 Hyp22]");
       try (iDestruct "Hyp22" as "[Hyp221 Hyp222]"); localAuto.
 
-    iInduction l as [| d l] "IHl" forall (l0); destruct l0 as [|d0 l0]; try done.
+    iInduction l as [| (l1, d1) ds1] "IHl" forall (l0); destruct l0 as [|(l2, d2) ds2]; try done.
     repeat iSplit;
-      try (iDestruct "Hyp" as "[Hyp1 Hyp2]"); localAuto.
+      try (iDestruct "Hyp" as "[% [Hyp1 Hyp2]]"); localAuto.
     by iApply "IHl".
   Qed.
 
diff --git a/theories/Dot/typing.v b/theories/Dot/typing.v
index efda74cc6..289bfa263 100644
--- a/theories/Dot/typing.v
+++ b/theories/Dot/typing.v
@@ -3,7 +3,7 @@ From D.Dot Require Import dotsyn.
 
 Reserved Notation "Γ ⊢ₜ e : T , i" (at level 74, e, T at next level).
 Reserved Notation "Γ ⊢ₚ p : T , i" (at level 74, p, T, i at next level).
-Reserved Notation "Γ ⊢ { l = d } : T" (at level 64, l, d, T at next level).
+Reserved Notation "Γ ⊢d d : T" (at level 64, d, T at next level).
 Reserved Notation "Γ ⊢ds ds : T" (at level 74, ds, T at next level).
 Reserved Notation "Γ ⊢ₜ T1 , i1 <: T2 , i2" (at level 74, T1, T2, i1, i2 at next level).
 
@@ -76,22 +76,24 @@ Inductive typed Γ: tm → ty → nat → Prop :=
     Γ ⊢ₜ t : TAnd T1 T2, i
 with dms_typed Γ: dms → ty → Prop :=
 | dnil_typed : Γ ⊢ds [] : TTop
+(* This demands definitions and members to be defined in aligned lists. I think
+   we want more freedom, just like in the logical relation? *)
 | dcons_typed l d ds T1 T2 :
-    Γ ⊢ds ds : T1 →
-    l = length ds →
-    Γ ⊢ { l = d } : T2 →
+    Γ ⊢d d : T1 →
+    Γ ⊢ds ds : T2 →
+    dms_hasnt ds l →
+    label_of_ty T1 = Some l →
     (*──────────────────────*)
-    Γ ⊢ds d :: ds : TAnd T1 T2
-
-with dm_typed Γ : label → dm → ty → Prop :=
+    Γ ⊢ds (l, d) :: ds : TAnd T1 T2
+with dm_typed Γ : dm → ty → Prop :=
 | dty_typed l L T U:
     Γ ⊢ₜ L, 0 <: U, 0 →
     Γ ⊢ₜ L, 1 <: T, 1 →
     Γ ⊢ₜ T, 1 <: U, 1 →
-    Γ ⊢ { l = dtysyn T } : TTMem l L U
+    Γ ⊢d dtysyn T : TTMem l L U
 | dvl_typed l v T:
     Γ ⊢ₜ tv v : TLater T, 0 →
-    Γ ⊢ { l = dvl v } : TVMem l T
+    Γ ⊢d dvl v : TVMem l T
 with path_typed Γ: path → ty → nat → Prop :=
 | pv_typed v T i:
     Γ ⊢ₜ tv v : T, i →
@@ -194,5 +196,5 @@ with subtype Γ : ty → nat → ty → nat → Prop :=
 where "Γ ⊢ₜ e : T , i" := (typed Γ e T i)
 and "Γ ⊢ₚ p : T , i" := (path_typed Γ p T i)
 and "Γ ⊢ds ds : T" := (dms_typed Γ ds T)
-and "Γ ⊢ { l = d } : T" := (dm_typed Γ l d T)
+and "Γ ⊢d d : T" := (dm_typed Γ d T)
 and "Γ ⊢ₜ T1 , i1 <: T2 , i2" := (subtype Γ T1 i1 T2 i2).
diff --git a/theories/Dot/typingExamples.v b/theories/Dot/typingExamples.v
index 66aca9446..9acf71845 100644
--- a/theories/Dot/typingExamples.v
+++ b/theories/Dot/typingExamples.v
@@ -4,6 +4,7 @@ I am also experimenting with notations, but beware the current definitions are p
  *)
 From D Require Import tactics.
 From D.Dot Require Import dotsyn typing.
+From stdpp Require Import strings.
 
 Implicit Types (L T U: ty) (v: vl) (e: tm) (d: dm) (ds: dms) (Γ : list ty).
 
@@ -17,43 +18,43 @@ Hint Constructors typed subtype dms_typed dm_typed path_typed.
 (** Notation for object values. *)
 Bind Scope dms_scope with dms.
 Open Scope dms_scope.
-Notation " {@ } " := (@nil dm) (format "{@ }") : dms_scope.
+Notation " {@ } " := (@nil (string * dm)) (format "{@ }") : dms_scope.
 Notation " {@ x } " := ( x :: {@} ) (format "{@  x  }"): dms_scope.
 Notation " {@ x ; y ; .. ; z } " := (cons x (cons y .. (cons z nil) ..)) (format "{@  x ;  y ;  .. ;  z  }"): dms_scope.
 Close Scope dms_scope.
 Arguments vobj _%dms_scope.
 
 Notation "'ν' ds " := (vobj ds) (at level 20, ds at next level).
-Notation "'val' = v" := (dvl v) (at level 20).
-Notation "'type' = T" := (dtysyn T) (at level 20).
+Notation "'val' l = v" := (l, dvl v) (at level 20, l at level 10).
+Notation "'type' l = T" := (l, dtysyn T) (at level 20, l at level 10).
 
 (** Notation for object types. *)
 Bind Scope ty_scope with ty.
 Open Scope ty_scope.
 (* Notation "⊤" := TTop : ty_scope. *)
 Notation " {@ } " := TTop (format "{@ }") : ty_scope.
-Notation " {@ T1 } " := ( TAnd {@} T1 ) (format "{@  T1  }"): ty_scope.
-Notation " {@ T1 ; T2 ; .. ; Tn } " := (TAnd .. (TAnd (TAnd {@} T1) T2) .. Tn)
+Notation " {@ T1 } " := ( TAnd T1 {@} ) (format "{@  T1  }"): ty_scope.
+Notation " {@ T1 ; T2 ; .. ; Tn } " := (TAnd T1 (TAnd T2 .. (TAnd Tn {@})..))
                                        (format "{@  T1  ;  T2  ;  ..  ;  Tn  }") : ty_scope.
 (* Notation " {@ T1 ; .. ; T2 ; Tn } " := (TAnd (TAnd .. (TAnd {@} T1) .. T2) Tn) *)
 (*                                          (format "{@  T1  ;  ..  ;  T2  ;  Tn  }"): ty_scope. *)
 Close Scope ty_scope.
 
 Notation "'μ' Ts " := (TMu Ts) (at level 20, Ts at next level).
-Notation "'type' l >: L <: U" := (TTMem l L U) (at level 0, l, L, U at level 10).
-Notation "'val' l : T" := (TVMem l T) (at level 0, l, T at level 10).
+Notation "'type' l >: L <: U" := (TTMem l L U) (at level 20, l, L, U at level 10).
+Notation "'val' l : T" := (TVMem l T) (at level 20, l, T at level 10).
 
-Check ν {@ val = vnat 0 }.
-Check ν {@ type = TTop }.
-Check ν {@ val = vnat 0; type = TTop }.
-Check μ {@ type 0 >: TNat <: TTop }.
-Check μ {@ val 0 : TNat }.
+Check ν {@ val "a" = vnat 0 }.
+Check ν {@ type "A" = TTop }.
+Check ν {@ val "a" = vnat 0; type "A" = TTop }.
+Check μ {@ type "A" >: TNat <: TTop }.
+Check μ {@ val "a" : TNat }.
 
 Check vobj {@}.
 Check ν {@ }.
-Check ν {@ val = vnat 0 }.
-Check ν {@ val = vnat 0 ; val = vnat 1 }.
-Check ν {@ val = vnat 0 ; type = TTop }.
+Check ν {@ val "a" = vnat 0 }.
+Check ν {@ val "a" = vnat 0 ; val "b" = vnat 1 }.
+Check ν {@ val "a" = vnat 0 ; type "A" = TTop }.
 
 (* Notation "v @ l1 @ .. @ l2 ; l" := (TSel (pself .. (pself (pv v) l1) .. l2) l) *)
 (*                                      (format "v  @  l1  @  ..  @  l2  ;  l", at level 69, l1, l2 at level 60). *)
@@ -62,9 +63,9 @@ Check ν {@ val = vnat 0 ; type = TTop }.
 Notation "v @ l1 @ .. @ l2" := (pself .. (pself (pv v) l1) .. l2)
                                      (format "v  @  l1  @  ..  @  l2", at level 69, l1, l2 at level 60).
 Notation "p @; l" := (TSel p l) (at level 71).
-Check (pv (var_vl 0) @; 1).
-Check (pself (pself (pv (var_vl 0)) 1) 2 @; 3).
-Check (var_vl 0 @ 1 @ 2 @; 3).
+Check (pv (var_vl 0) @; "A").
+Check (pself (pself (pv (var_vl 0)) "A") "B" @; "C").
+Check (var_vl 0 @ "A" @ "B" @; "C").
 
 Example ex0 e Γ T i:
   Γ ⊢ₜ e : T, i →
@@ -80,7 +81,7 @@ Qed.
 Local Notation "Γ ⊢ds ds : T"  := (dms_typed Γ ds T) (at level 74, ds, T at next level).
 
 Example ex1 Γ n T:
-  Γ ⊢ₜ tv (ν {@ val = vnat n}) : μ {@ val 0 : TNat }, 0.
+  Γ ⊢ₜ tv (ν {@ val "a" = vnat n}) : μ {@ val "a" : TNat }, 0.
 Proof.
   (* Help proof search: *)
   apply VObj_typed. (* Avoid trying TMuI_typed, that's slow. *)
@@ -101,12 +102,12 @@ Proof.
     intro.
     eapply Trans_stp; by [apply TSucc_stp | apply TLaterR_stp].
   }
-  naive_solver.
+  constructor; naive_solver.
 Qed.
 
 Example ex2 Γ T:
-  Γ ⊢ₜ tv (vobj [dtysyn (TSel (pv (var_vl 0)) 0)]) :
-    TMu (TAnd TTop (TTMem 0 TBot TTop)), 0.
+  Γ ⊢ₜ tv (vobj [("A", dtysyn (TSel (pv (var_vl 0)) "B"))]) :
+    TMu (TAnd (TTMem "A" TBot TTop) TTop), 0.
 Proof.
   apply VObj_typed.
   econstructor => //=.
@@ -115,11 +116,11 @@ Qed.
 
 (* Try out fixpoints. *)
 Definition F3 T :=
-  TMu (TAnd TTop (TTMem 0 T T)).
+  TMu (TAnd (TTMem "A" T T) TTop).
 
 Example ex3 Γ T:
-  Γ ⊢ₜ tv (ν {@ type = (F3 (TSel (pv (var_vl 0)) 0)) } ) :
-    F3 (F3 (TSel (pv (var_vl 0)) 0)), 0.
+  Γ ⊢ₜ tv (ν {@ type "A" = (F3 (TSel (pv (var_vl 0)) "A")) } ) :
+    F3 (F3 (TSel (pv (var_vl 0)) "A")), 0.
 Proof.
   apply VObj_typed. (* Avoid trying TMuI_typed, that's slow. *)
   econstructor => //=.
@@ -138,13 +139,13 @@ Qed.
 (* Abort. *)
 
 Definition F4 T :=
-  TMu (TAnd (TAnd TTop (TTMem 0 T T))
-            (TVMem 1 (TSel (pv (var_vl 0)) 0))).
+  TMu (TAnd (TVMem "A" (TSel (pv (var_vl 0)) "B")) (TAnd (TTMem "B" T T) TTop)).
 Print F4.
 
+(* XXX Not sure I got this right. *)
 Example ex4 Γ T:
-  Γ ⊢ₜ tv (ν {@ val = var_vl 0; type = TSel (pv (var_vl 0)) 0 }) :
-    F4 (F4 (TSel (pv (var_vl 0)) 0)), 0.
+  Γ ⊢ₜ tv (ν {@ val "a" = var_vl 0; type "B" = TSel (pv (var_vl 0)) "A" }) :
+    F4 (F4 (TSel (pv (var_vl 0)) "A")), 0.
 Abort.
 (*     (* TMu (TAnd (TAnd TTop (TTMem 0 ?))  *) *)
 (*     (*                      (TVMem 1 (TSel (pv (var_vl 0)) 0))). *) *)
diff --git a/theories/Dot/unary_lr.v b/theories/Dot/unary_lr.v
index 2129c11e5..06139927f 100644
--- a/theories/Dot/unary_lr.v
+++ b/theories/Dot/unary_lr.v
@@ -148,40 +148,35 @@ Section logrel.
     Persistent (⟦ T ⟧ ρ v).
   Proof. revert v ρ; induction T => v ρ; simpl; try apply _. Qed.
 
-  Program Fixpoint def_interp (T: ty) (l : label) :
+  Program Fixpoint def_interp (T: ty) :
     listVlC -n> dmC -n> iProp Σ :=
     λne ρ d,
     match T with
-    | TTMem l' L U => ⌜ l = l' ⌝ ∧ def_interp_tmem (interp L) (interp U) ρ d
-    | TVMem l' T' => ⌜ l = l' ⌝ ∧ def_interp_vmem (interp T') ρ d
+    | TTMem _ L U => def_interp_tmem (interp L) (interp U) ρ d
+    | TVMem _ T' => def_interp_vmem (interp T') ρ d
     | _ => False
     end%I.
 
-  Global Instance def_interp_persistent T l ρ d :
-    Persistent (def_interp T l ρ d).
+  Global Instance def_interp_persistent T ρ d :
+    Persistent (def_interp T ρ d).
   Proof. revert ρ d; induction T; simpl; try apply _. Qed.
 
-  Program Definition defs_interp_and
-             (interp1 : listVlC -n> dmsC -n> iProp Σ)
-             (interp2: label -> listVlC -n> dmC -n> iProp Σ)
-    : listVlC -n> dmsC -n> iProp Σ :=
-    λne ρ ds,
-    match ds with
-    | [] => False
-    | d :: ds => interp1 ρ ds ∧ interp2 (length ds) ρ d
-    end%I.
+  Program Definition defs_interp_and (interp1 interp2 : listVlC -n> dmsC -n> iProp Σ) :
+    listVlC -n> dmsC -n> iProp Σ :=
+    λne ρ ds, (interp1 ρ ds ∧ interp2 ρ ds)%I.
 
   Program Fixpoint defs_interp (T: ty) : listVlC -n> dmsC -n> iProp Σ :=
     match T with
-    | TAnd T1 T2 => defs_interp_and (defs_interp T1) (def_interp T2)
+    | TAnd T1 T2 => defs_interp_and (defs_interp T1) (defs_interp T2)
     | TTop => λne ρ ds, ⌜ nclosed ds 0 ⌝
-    | _ => λne ρ ds, False
+    | _ => λne ρ ds,
+           ∃ l d,
+             ⌜ label_of_ty T = Some l ∧ dms_lookup l ds = Some d ∧ nclosed ds 0 ⌝
+             ∧ def_interp T ρ d
     end % I.
 
-  Global Instance defs_interp_persistent T ρ ds :
-    Persistent (defs_interp T ρ ds).
-  Proof.
-    revert ds ρ; induction T; simpl; intros; try case_match; try apply _.
+  Global Instance defs_interp_persistent T ρ ds : Persistent (defs_interp T ρ ds).
+  Proof. revert ds ρ; induction T; cbn; try case_match; try apply _.
   Qed.
 
   Fixpoint interp_env (Γ : ctx) (vs : vls) : iProp Σ :=
@@ -206,12 +201,12 @@ Section logrel.
 
   (** Definitions for semantic (definition) (sub)typing *)
   (** Since [⟦Γ⟧* ρ] might be impossible, we must require closedness explicitly. *)
-  Definition idtp Γ T l d : iProp Σ :=
-    (⌜ nclosed d (length Γ) ⌝ ∗ □∀ ρ, ⟦Γ⟧* ρ → def_interp T l ρ d.|[to_subst ρ])%I.
+  Definition idtp Γ T d : iProp Σ :=
+    (⌜ nclosed d (length Γ) ⌝ ∗ □∀ ρ, ⟦Γ⟧* ρ → def_interp T ρ d.|[to_subst ρ])%I.
   Global Arguments idtp /.
-  Notation "Γ ⊨d { l = d } : T" := (idtp Γ T l d) (at level 64, l, d, T at next level).
+  Notation "Γ ⊨d d : T" := (idtp Γ T d) (at level 64, d, T at next level).
 
-  Lemma idtp_closed Γ T l d: (Γ ⊨d {l = d} : T → ⌜ nclosed d (length Γ) ⌝)%I.
+  Lemma idtp_closed Γ T d: (Γ ⊨d d : T → ⌜ nclosed d (length Γ) ⌝)%I.
   Proof. iIntros "[$ _]". Qed.
 
   Definition idstp Γ T ds : iProp Σ :=
@@ -253,7 +248,7 @@ Section logrel.
     (□∀ ρ v, ⌜ nclosed_vl v 0 ⌝ → ⟦Γ⟧*ρ → (▷^i ⟦T1⟧ ρ v) → ▷^j ⟦T2⟧ ρ v)%I.
   Global Arguments step_indexed_ivstp /.
 
-  Global Instance idtp_persistent Γ T l d: Persistent (idtp Γ T l d) := _.
+  Global Instance idtp_persistent Γ T d: Persistent (idtp Γ T d) := _.
   Global Instance idstp_persistent Γ T ds: Persistent (idstp Γ T ds) := _.
   Global Instance ietp_persistent Γ T e : Persistent (ietp Γ T e) := _.
   Global Instance step_indexed_ietp_persistent Γ T e i : Persistent (step_indexed_ietp Γ T e i) := _.
@@ -266,7 +261,7 @@ Notation "⟦ Γ ⟧*" := (interp_env Γ).
 Notation "⟦ T ⟧ₑ" := (interp_expr (interp T)).
 
 (** Single-definition typing *)
-Notation "Γ ⊨d { l = d } : T" := (idtp Γ T l d) (at level 64, l, d, T at next level).
+Notation "Γ ⊨d d : T" := (idtp Γ T d) (at level 64, d, T at next level).
 (** Multi-definition typing *)
 Notation "Γ ⊨ds ds : T" := (idstp Γ T ds) (at level 74, ds, T at next level).
 (** Expression typing *)
diff --git a/theories/Dot/unary_lr_binding.v b/theories/Dot/unary_lr_binding.v
index aa839a3ff..2f5a51473 100644
--- a/theories/Dot/unary_lr_binding.v
+++ b/theories/Dot/unary_lr_binding.v
@@ -10,19 +10,16 @@ Implicit Types
 Section logrel_binding_lemmas.
   Context `{HdotG: dotG Σ}.
 
-  Lemma def_interp_v_closed T d l ρ: (def_interp T l ρ d → ⌜ nclosed d 0 ⌝)%I.
+  Lemma def_interp_v_closed T d ρ: (def_interp T ρ d → ⌜ nclosed d 0 ⌝)%I.
   Proof.
-    iInduction T as [] "IH" forall (ρ d); iIntros "#HT //="; by iDestruct "HT" as "[% [% _]]".
+    iInduction T as [] "IH" forall (ρ d); iIntros "#HT //="; by iDestruct "HT" as "[% _]".
   Qed.
 
   Lemma defs_interp_v_closed T ds ρ: (defs_interp T ρ ds → ⌜ nclosed ds 0 ⌝)%I.
   Proof.
-    iInduction T as [] "IH" forall (ρ ds); iIntros "#HT //=".
-    destruct ds. done.
-    iDestruct "HT" as "[HT1 HT2]".
-    iPoseProof ("IH" with "HT1") as "%".
-    iPoseProof (def_interp_v_closed with "HT2") as "%".
-    iPureIntro. by apply fv_dms_cons.
+    iInduction T as [] "IH" forall (ρ ds);
+      iIntros "#HT //="; try iDestruct "HT" as (l1 d) "[% ?]"; ev; trivial.
+    iDestruct "HT" as "[HT1 _]"; by iApply "IH".
   Qed.
 
   Lemma interp_weaken ρ1 ρ2 ρ3 τ :