diff --git a/F_mu_ref_conc/binder.v b/F_mu_ref_conc/binder.v
index 6b574379a187a5b9d6231892660e76f165bfc80a..229272c143410d18f15eafeead8ecb81efea8b8c 100644
--- a/F_mu_ref_conc/binder.v
+++ b/F_mu_ref_conc/binder.v
@@ -1,6 +1,6 @@
 (* This module defines binders and liftings of all the necessary
 operations/lemmas. *)
-From stdpp Require Import strings gmap mapset stringmap.
+From iris_logrel.prelude Require Export base.
 From iris.algebra Require Export base.
 
 Inductive binder := BAnon | BNamed : string → binder.
@@ -44,16 +44,6 @@ Instance singleton_binder_set : Singleton binder stringset :=
        end.
 
 (** Properties lifts *)
-(* TODO: move this somewhere else *)
-Lemma difference_empty_map {K A} `{EqDecision K} `{Countable K} (X : gmap K A) :
-  X ∖ ∅ = X.
-Proof.
-  apply map_eq => i.
-  remember (X !! i) as Z. destruct Z.
-  - apply lookup_difference_Some. split; eauto.
-  - apply lookup_difference_None. left; eauto.
-Qed.
-
 Lemma dom_delete_binder {A} (i : binder) (m : stringmap A) :
   dom (gset string) (delete i m) ≡ (dom (gset string) m) ∖ {[i]}.
 Proof.
@@ -77,21 +67,6 @@ Lemma cons_binder_union (i : binder) (X : gset string) :
   i :b: X = {[i]} ∪ X.
 Proof. destruct i; cbn-[union]; eauto. set_solver. Qed.
 
-(* TODO: move this somewhere else *)
-Lemma singleton_union_difference (X Y : stringset) (x : string) :
-  {[x]} ∪ (X ∖ Y) = ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
-Proof.
-    unfold_leibniz. intros y. split; intro Hy. 
-    - apply elem_of_union in Hy. set_solver.
-    - apply elem_of_difference in Hy. destruct Hy as [Hy1 Hy2].
-      apply elem_of_union in Hy1.          
-      rewrite elem_of_union. rewrite elem_of_difference.
-      rewrite elem_of_singleton.
-      destruct (decide (x = y)); subst; eauto.
-      assert (y ∉ {[x]}). intro K; apply elem_of_singleton in K. auto.
-      right. destruct Hy1; set_solver.
-Qed.
-
 Lemma lookup_insert_binder {A} (i : binder) (j : string) (x : A) (m : stringmap A):
   i = BNamed j → <[i:=x]>m !! j = Some x.
 Proof. intros ->. apply lookup_insert. Qed.
@@ -152,10 +127,6 @@ Lemma delete_commute_binder {A} (m : stringmap A) (i j : binder) :
   delete i (delete j m) = delete j (delete i m).
 Proof. destruct i, j; cbn; auto. apply delete_commute. Qed.
 
-(* TODO: move it to stdpp *)
-Lemma delete_singleton_ne {A} (i j : string) (x : A) : j ≠ i → delete i {[j := x]} = {[j := x]}.
-Proof. intros Hij. apply delete_notin. by apply lookup_singleton_ne. Qed.
-
 Lemma delete_empty_binder {A} (x : binder) :
   delete x (∅ : stringmap A) = ∅.
 Proof. destruct x; cbn; eauto. apply delete_empty. Qed.
@@ -181,3 +152,9 @@ Proof.
   destruct x; cbn; auto.
   by rewrite fmap_insert.
 Qed.
+
+Lemma delete_idem_binder {A} (x : binder) (m : stringmap A) :
+  delete x (delete x m) = delete x m.
+Proof.
+  destruct x; cbn; eauto. apply delete_idem.
+Qed.
diff --git a/F_mu_ref_conc/examples/counter.v b/F_mu_ref_conc/examples/counter.v
index 80452667c8bf4e18377db268829c0d30d2459887..011cfa9df0a9de726a4dba7312fac9346ed29acf 100644
--- a/F_mu_ref_conc/examples/counter.v
+++ b/F_mu_ref_conc/examples/counter.v
@@ -42,28 +42,6 @@ Section CG_Counter.
     repeat econstructor; eauto; cbn; seq_map_lookup.
   Qed.
 
-  (* TODO: this is copypasta from lock.v *)
-  Tactic Notation "rel_bind_l" open_constr(efoc) :=
-    iStartProof;
-    lazymatch goal with
-    | [ |- (_ ⊢ bin_log_related _ _ _ (fill _ ?e) _ _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
-    | [ |- (_ ⊢ bin_log_related _ _ _ ?e _ _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
-    end.
-  Tactic Notation "rel_bind_r" open_constr(efoc) :=
-    iStartProof;
-    lazymatch goal with
-    | [ |- (_ ⊢ bin_log_related _ _ _ _ (fill _ ?e) _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
-    | [ |- (_ ⊢ bin_log_related _ _ _ _ ?e _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
-    end.
-
   Lemma steps_CG_increment E ρ j K x n:
     nclose specN ⊆ E →
     spec_ctx ρ -∗ x ↦ₛ (#nv n)
@@ -383,6 +361,32 @@ Section CG_Counter.
       iApply "IH".
   Qed.    
 
+  (* Lemma wp_step_back Γ (e t : expr) (x : string) (v ev : val) τ : *)
+  (*   Closed ∅ (Lam x e) → *)
+  (*   to_val (lang.subst x (of_val v) e) = Some ev → *)
+  (*   Γ ⊨ (App (Lam x e) v) ≤log≤ t : τ *)
+  (*   ⊢ Γ ⊨ (lang.subst x (of_val v) e) ≤log≤ t : τ. *)
+  (* Proof. *)
+  (*   iIntros (??) "Hr". *)
+  (*   Transparent bin_log_related. *)
+  (*   iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj". *)
+  (*   cbn-[subst_p].  *)
+  (*   (* assert (Closed ∅ (lang.subst x v e)). *) *)
+  (*   (* { eapply is_closed_subst_preserve; eauto. solve_closed. } *) *)
+  (*   rewrite /env_subst !Closed_subst_p_id. *)
+  (*   iSpecialize ("Hr" with "Hs []"). *)
+  (*   { iAlways. by iFrame. } *)
+  (*   rewrite /env_subst. erewrite (Closed_subst_p_id (fst <$> vvs)); last first. *)
+  (*   { rewrite /Closed. simpl. *)
+  (*     rewrite /Closed /= in H1. split_and; eauto; try solve_closed. } *)
+  (*   iMod ("Hr" with "Hj") as "Hr". *)
+  (*   iModIntro. simpl. *)
+  (*   rewrite {1}wp_unfold /wp_pre /=. *)
+  (*   iApply wp_value; eauto. *)
+  (*   iApply (wp_bind_inv in "Hr". *)
+  (*   Opaque bin_log_related. *)
+
+
   (* TODO: try to use with_lock rules *)
   Lemma FG_CG_increment_refinement l cnt cnt' Γ :
     inv counterN (counter_inv l cnt cnt') -∗
diff --git a/F_mu_ref_conc/examples/lock.v b/F_mu_ref_conc/examples/lock.v
index eb98def70a7051e929c6b9e79f1c4ad54725fb9c..4007218527805c9daf16e0956f1966a75cdb2933 100644
--- a/F_mu_ref_conc/examples/lock.v
+++ b/F_mu_ref_conc/examples/lock.v
@@ -12,9 +12,6 @@ Definition acquire : val :=
            (Unit)
            (App "acquire" "x")).
 
-(* TODO: move to notation.v *)
-Coercion of_val : val >-> expr.
-
 (** [release = λ x. x <- false] *)
 Definition release : val := LamV "x" (Store "x" (#♭ false)).
 (** [with_lock e l = λ x. (acquire l) ;; e x ;; (release l)] *)
@@ -109,29 +106,6 @@ Section proof.
     by iFrame.
   Qed.  
   
-  (* TODO: those should be accompaied by lemmas; preferably so that 
-     [change] does not change too much *)
-  Tactic Notation "rel_bind_l" open_constr(efoc) :=
-    iStartProof;
-    lazymatch goal with
-    | [ |- (_ ⊢ bin_log_related _ _ _ (fill _ ?e) _ _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e'))
-    | [ |- (_ ⊢ bin_log_related _ _ _ ?e _ _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e'))
-    end.
-  Tactic Notation "rel_bind_r" open_constr(efoc) :=
-    iStartProof;
-    lazymatch goal with
-    | [ |- (_ ⊢ bin_log_related _ _ _ _ (fill _ ?e) _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
-    | [ |- (_ ⊢ bin_log_related _ _ _ _ ?e _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
-    end.
-
   Lemma bin_log_related_acquire_r Γ E1 E2 K l t τ
     (Hspec : nclose specN ⊆ E1) :
     l ↦ₛ (#♭v false) -∗
diff --git a/F_mu_ref_conc/fundamental_binary.v b/F_mu_ref_conc/fundamental_binary.v
index fb1da9ab5be22a951c66015c04fc489b7b564132..6a648e82601367db796b915f1f9b382a64f0a95d 100644
--- a/F_mu_ref_conc/fundamental_binary.v
+++ b/F_mu_ref_conc/fundamental_binary.v
@@ -28,7 +28,7 @@ Section masked.
     let vh := iFresh in
     iIntros vh;
     try (iMod vh);
-    iDestruct vh as (w) (String.append "[Hj " (String.append Hv " ]")); simpl. (* ; iApply fupd_wp. *)
+    iDestruct vh as (w) (String.append "[Hj " (String.append Hv " ]")); simpl.
 
   Lemma bin_log_related_var Γ x τ : 
     Γ !! x = Some τ →
@@ -125,28 +125,7 @@ Section masked.
     iSpecialize ("IH1" with "IH2 Hj").    
     by iMod "IH1". 
   Qed.
-  
-  (* TODO: move to std++ *)
-  Lemma difference_union_id {A : Type} `{EqDecision A, Countable A} (X Y : gset A):
-    X ∖ Y ∪ Y = X ∪ Y.
-  Proof.
-    unfold_leibniz. intro x.
-    rewrite !elem_of_union elem_of_difference.
-    split.
-    - set_solver.
-    - destruct (decide (x ∈ Y)); set_solver.
-  Qed.
-  (* TODO: move to std++ *)
-  Lemma difference_empty {A: Type} `{EqDecision A, Countable A} (X : gset A) :
-    X ∖ ∅ = X.
-  Proof.
-    unfold_leibniz.
-    rewrite <- (right_id ∅ union (X ∖ ∅)).
-    rewrite <- (right_id ∅ union X) at 2.
-    fold_leibniz.
-    apply difference_union_id.
-  Qed.
-  
+    
   Lemma bin_log_related_rec (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
     Closed (x :b: f :b: dom _ Γ) e →
     Closed (x :b: f :b: dom _ Γ) e' →
diff --git a/F_mu_ref_conc/notation.v b/F_mu_ref_conc/notation.v
index 4a1de034c0f5aa933f9acf9061b720e43e8933b4..cbf2bf05db05991c3d425a57e943dcf1ebba58f0 100644
--- a/F_mu_ref_conc/notation.v
+++ b/F_mu_ref_conc/notation.v
@@ -67,3 +67,4 @@ Notation "'Λ:' e" := (TLam e%E)
 Notation "'Λ:' e" := (TLamV e%E)
   (at level 102, e at level 200) : val_scope.
 
+Coercion of_val : val >-> expr.
diff --git a/F_mu_ref_conc/relational_properties.v b/F_mu_ref_conc/relational_properties.v
index a99cef77ebeb8e04a04da5b6a224baeb3830274d..433f57eaddb5dae595cefba9c69d0dbc7c4520a8 100644
--- a/F_mu_ref_conc/relational_properties.v
+++ b/F_mu_ref_conc/relational_properties.v
@@ -14,31 +14,6 @@ Section properties.
   (** * Lemmas to show that binary logical model is closed under
   (forward) reductions. *)
 
-  (* Lemma interp_expr_mono (E E' : coPset) Δ τ : *)
-  (*   (E ⊆ E') → *)
-  (*   (∀ v, interp_expr E E (interp E E τ) Δ v -∗ interp_expr E' E' (interp E E τ) Δ v)%I. *)
-  (* Proof. *)
-  (*   iIntros (?). *)
-  (*   iInduction τ as [] "IH"; simpl; iIntros (v) "H"; *)
-  (*     iIntros (j K) "Hj"; iSpecialize ("H" with "* Hj"); *)
-  (*     iApply (wp_mask_mono E); auto; *)
-  (*     iApply fupd_wp; auto. *)
-  (* Qed. *)
-  (* Lemma interp_expr_mono2 (E E' : coPset) (P Q : listC D -n> D) Δ : *)
-  (*   (E ⊆ E') → *)
-  (*   (∀ (x : listC D) w, P x w -∗ Q x w) -∗ *)
-  (*   (∀ v, interp_expr E E P Δ v -∗ interp_expr E' E' Q Δ v)%I. *)
-  (* Proof. *)
-  (*   iIntros (?) "HPQ". iIntros (vv) "H". *)
-  (*   iIntros (j K) "Hj". iSpecialize ("H" with "Hj"). iModIntro. *)
-  (*   iApply (wp_mask_mono E); auto. *)
-  (*   iApply fupd_wp; auto. *)
-  (*   iMod "H". iModIntro. *)
-  (*   iApply (wp_wand with "H [HPQ]"). *)
-  (*   iIntros (v) "Hv". iDestruct "Hv" as (v') "[Hj HP]". *)
-  (*   iExists _; iFrame. by iApply "HPQ". *)
-  (* Qed.     *)
-
   (* We need this to be able to open and closed invariants in front of logrels *)
   Lemma fupd_logrel Γ E1 E2 e e' τ :
     ((|={E1,E2}=> ({E2,E2;Γ} ⊨ e ≤log≤ e' : τ))
@@ -738,8 +713,6 @@ Section properties.
     econstructor; eauto.
   Qed.
   
-  (* TODO difference btween |={⊤}=> and |==>  *)
-  (*   note: also can put an update after the quantifier (in addition to the one present *)
   (** Stateful reductions *)
   Lemma bin_log_related_step_r Φ Γ E1 E2 K' e1 e2 τ
     (Hclosed2 : Closed ∅ e2) :
@@ -866,5 +839,27 @@ Section properties.
 
   (* To prevent accidental unfolding by iMod or other tactics *)
   Typeclasses Opaque bin_log_related.
-
 End properties.
+
+(* TODO: those should be accompaied by lemmas; preferably so that 
+   [change] does not change too much *)
+Tactic Notation "rel_bind_l" open_constr(efoc) :=
+  iStartProof;
+  lazymatch goal with
+  | [ |- (_ ⊢ bin_log_related _ _ _ (fill _ ?e) _ _ ) ] =>
+    reshape_expr e ltac:(fun K e' =>
+     unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
+  | [ |- (_ ⊢ bin_log_related _ _ _ ?e _ _ ) ] =>
+    reshape_expr e ltac:(fun K e' =>
+     unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
+  end.
+Tactic Notation "rel_bind_r" open_constr(efoc) :=
+  iStartProof;
+  lazymatch goal with
+  | [ |- (_ ⊢ bin_log_related _ _ _ _ (fill _ ?e) _ ) ] =>
+    reshape_expr e ltac:(fun K e' =>
+     unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
+  | [ |- (_ ⊢ bin_log_related _ _ _ _ ?e _ ) ] =>
+    reshape_expr e ltac:(fun K e' =>
+     unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
+  end.
diff --git a/F_mu_ref_conc/subst.v b/F_mu_ref_conc/subst.v
index ff8ea7ba08a2a7eb48441768a31886336b90e1db..a8e0a9f3dd3f22e0a8efb934c705ec5c12d51dd6 100644
--- a/F_mu_ref_conc/subst.v
+++ b/F_mu_ref_conc/subst.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export ectx_language ectxi_language.
 From iris.algebra Require Export ofe.
-From stdpp Require Import strings gmap mapset stringmap.
+From iris_logrel.prelude Require Export base.
 From iris_logrel.F_mu_ref_conc Require Export binder lang.
 
 (** Definitions and properties about substitution and closedness *)
@@ -311,200 +311,72 @@ Proof.
   }
 Admitted.
 
-
-  (* Lemma subst_p_closed X Y es e :  *)
-  (*   Closed Y e → Y ⊆ dom _ es → *)
-  (*   Closed X (subst_p es e). *)
-  (* Proof. *)
-  (*   replace X with (X ∪ ∅) by set_solver. *)
-  (*   replace (dom stringset es) with (dom stringset es ∪ ∅) by set_solver. *)
-  (*   eapply subst_p_allClosed'. *)
-  (* Qed. *)
-
-  (* Lemma subst_p_commute (vs vs': stringmap expr) e X : *)
-  (*   allClosed X vs' → *)
-  (*   X ⊥ (dom _ vs) → *)
-  (*   subst_p vs (subst_p vs' e) = subst_p (vs' ∪ vs) e. *)
-  (* Proof. *)
-  (*   revert X vs vs'. induction e => X vs vs' /= Hcl Hort /=; *)
-  (*   try by (repeat lazymatch goal with *)
-  (*   | [IH: context[subst_p _ (subst_p _ ?e) = subst_p _ ?e] *)
-  (*      |- context[subst_p _ (subst_p _ ?e)] ] =>  *)
-  (*     erewrite IH *)
-  (*   end; eauto). *)
-  (*   - remember (vs' !! x) as Hx1. destruct Hx1. *)
-  (*     + erewrite lookup_union_Some_l; eauto. rewrite -HeqHx1. f_equal. *)
-  (*       symmetry. eapply subst_p_closed. eapply Hcl; eauto. *)
-  (*       intros y Hy. eapply not_elem_of_dom. intro Hydom. *)
-  (*       eapply (proj1 (elem_of_disjoint X (dom stringset vs)) Hort); eauto. *)
-  (*     + remember (vs !! x) as Hx2. destruct Hx2.  *)
-  (*       * assert ((vs' ∪ vs) !! x = Some e) as ->. *)
-  (*         apply lookup_union_Some_raw. right. split; eauto. *)
-  (*         simplify_map_eq. done. *)
-  (*       * assert ((vs' ∪ vs) !! x = None) as ->. *)
-  (*         apply lookup_union_None. split; auto. *)
-  (*         simplify_map_eq. done. *)
-  (*   - erewrite IHe; eauto. *)
-  (*     + f_equal. f_equal. *)
-  (*       destruct f,x; cbn; rewrite ?delete_union; done. *)
-  (*     + eapply (allClosed_mono_2 vs'). destruct f,x; cbn; try fast_done; try eapply delete_subseteq. etransitivity; eapply delete_subseteq. *)
-  (*       eassumption. *)
-  (*     + rewrite ?dom_delete_binder. destruct x,f; set_solver. *)
-  (* Qed. *)
-  
-  (* Lemma Closed_subst_p es e `{Closed X e} `{allClosed X es} : Closed X (subst_p es e). *)
-  (* Proof. *)
-  (*   generalize dependent X. generalize dependent es. *)
-  (*   induction e => es X HXe HXes /=; rewrite /allClosed in HXes; rewrite /Closed /=; *)
-  (*   unfold Closed in *; *)
-  (*   simpl in HXe; *)
-  (*   destruct_and?; split_and?; *)
-  (*   try (lazymatch goal with *)
-  (*   | [IH: context[is_closed _ (subst_p _ ?e)] *)
-  (*      |- Is_true (is_closed ?X (subst_p ?es ?e)) ] => *)
-  (*     eapply (IH es X) *)
-  (*   end); eauto. *)
-  (*   - specialize (HXes x). destruct (es !! x); cbn; eauto.  *)
-  (*   - intros i e'.  *)
-  (*     destruct f as [|f], x as [|x]; simpl; cbn-[union]; cbn-[union] in HXe; eauto; *)
-  (*       try destruct (decide (x = i));  *)
-  (*       try destruct (decide (f = i)); subst; *)
-  (*       repeat match goal with *)
-  (*       | [ |- context[delete ?i _ !! ?i = Some _] ] =>  *)
-  (*         rewrite lookup_delete *)
-  (*       | [ |- context[delete ?x _ !! ?i = Some _] ] =>  *)
-  (*         rewrite lookup_delete_ne *)
-  (*       end;  *)
-  (*       try by (inversion 1); eauto. *)
-  (*       all: (intro H; eapply Closed_mono; first (eapply HXes); eauto; *)
-  (*       set_solver). *)
-  (* Qed. *)
-
-  (* Lemma subst_subst_ne e x y es es' : *)
-  (*   Closed ∅ es → Closed ∅ es' → x ≠ y → *)
-  (*   subst x es (subst y es' e) = subst y es' (subst x es e). *)
-  (* Proof. *)
-  (*   intros. induction e; simpl; try (f_equal; by auto); *)
-  (*     simplify_option_eq; auto using eq_sym, subst_is_closed_empty with f_equal. *)
-  (* Qed. *)
-
-  (* Lemma beta_subst_allClosed x f e e' v : *)
-  (*   to_val e' = Some v → *)
-  (*   Closed (x :b: f :b: ∅) e → *)
-  (*   allClosed ∅ (<[x:=e']>{[f:=Rec f x e]}). *)
-  (* Proof. rewrite ?cons_binder_union. *)
-  (*   intros He' Hcl. intros i j. *)
-  (*   rewrite -(of_to_val e' v He'). *)
-  (*   destruct f,x; cbn-[union]; eauto. *)
-  (*   - rewrite lookup_empty. inversion 1. *)
-  (*   - destruct (decide (i = s)); subst; eauto. *)
-  (*     + rewrite lookup_insert. injection 1. intro; subst. *)
-  (*       apply val_closed. *)
-  (*     + rewrite lookup_insert_ne; auto. *)
-  (*       rewrite lookup_empty. inversion 1. *)
-  (*   - destruct (decide (i = s)); subst; eauto. *)
-  (*     + rewrite lookup_insert. injection 1. intro; subst. *)
-  (*       simpl. cbn-[union] in Hcl.  *)
-  (*       rewrite /Closed in Hcl. *)
-  (*       replace (is_closed ({[s]} ∪ ∅) e) *)
-  (*       with (is_closed (∅ ∪ ({[s]} ∪ ∅)) e). done. *)
-  (*       f_equal. set_solver. *)
-  (*     + rewrite lookup_insert_ne; auto. *)
-  (*       rewrite lookup_empty. inversion 1. *)
-  (*   - destruct (decide (i = s0)); subst; eauto. *)
-  (*     + rewrite lookup_insert. injection 1. intro; subst. *)
-  (*       apply val_closed. *)
-  (*     + rewrite lookup_insert_ne; auto. *)
-  (*       destruct (decide (i = s)); subst; auto. *)
-  (*       * rewrite lookup_insert. injection 1. intro; subst. auto. *)
-  (*       * rewrite lookup_insert_ne; auto. *)
-  (*         rewrite lookup_empty. inversion 1. *)
-  (* Qed. *)
-
-  (* TODO: move to std++ *)
-  Lemma delete_insert_delete {A} (m : stringmap A) (i : string) (x : A) :
-    delete i (<[i:=x]> m) = delete i m.
-  Proof.
-    apply map_eq=>j.
-    destruct (decide (i = j)) as [Eij|Nij];
-      simplify_map_eq; auto.
-  Qed.
-
-  Lemma subst_p_insert (x : binder) v (m : stringmap val) e :
-    subst_p (<[x:=v]>m) e =
-    (subst_p m (subst' x (of_val v) e)).
-  Proof. 
-    generalize dependent m.
-    destruct x as [|x]; cbn; auto.
-    induction e; simpl; intro m; auto 10 with f_equal;
-    repeat match goal with
-    | [ IH : subst_p _ _ = subst' _ _ _  |- _ ] => 
-      rewrite IH; clear IH
-    end.
-    - simplify_option_eq.
-      + rewrite lookup_insert. by rewrite Closed_subst_p_id.
-      + by rewrite lookup_insert_ne.
-    - f_equal. simplify_option_eq.
-      + destruct_and!. 
-        rewrite !delete_insert_ne_binder' //.
-      + apply not_and_l in H as [<-%dec_stable|<-%dec_stable].
-        * rewrite delete_commute_binder.
-          cbn[delete delete_binder].
-          rewrite delete_insert_delete.
-          rewrite (delete_commute_binder _ x0 (BNamed x)).
-          reflexivity.
-        * cbn[delete delete_binder].
-          rewrite delete_insert_delete.
-          reflexivity.
-  Qed.
-  
-  (* TODO: move to std++ *)
-  Lemma delete_delete {A} (x : binder) (m : stringmap A) :
-    delete x (delete x m) = delete x m.
-  Proof.
-    destruct x as [|x]; cbn; eauto.
-    rewrite delete_notin; first done.
-    apply lookup_delete.
-  Qed.
-  
-  Lemma subst_p_delete (x : binder) (e' : expr) (m : stringmap val) e `{Closed ∅ e'} :
-    subst_p m (subst' x e' e) =
-    subst' x e' (subst_p (delete x m) e).
-  Proof.
-    generalize dependent m.
-    destruct x as [|x]; cbn; auto.
-    induction e; simpl; intro m; auto 10 with f_equal;
-    repeat match goal with
-    | [ IH : subst_p _ _ = subst' _ _ _  |- _ ] => 
-      rewrite IH; clear IH
-    end.
-    - simplify_option_eq.
-      + rewrite lookup_delete. 
-        rewrite Closed_subst_p_id. simpl. by rewrite decide_left.
-      + rewrite lookup_delete_ne; auto.
-        case_match.
-        * by rewrite Closed_subst_id.
-        * simpl. by rewrite decide_False.
-    - f_equal. simplify_option_eq.
-      + destruct_and!. 
+Lemma subst_p_insert (x : binder) v (m : stringmap val) e :
+  subst_p (<[x:=v]>m) e =
+  (subst_p m (subst' x (of_val v) e)).
+Proof. 
+  generalize dependent m.
+  destruct x as [|x]; cbn; auto.
+  induction e; simpl; intro m; auto 10 with f_equal;
+  repeat match goal with
+  | [ IH : subst_p _ _ = subst' _ _ _  |- _ ] => 
+  rewrite IH; clear IH
+  end.
+  - simplify_option_eq.
+    + rewrite lookup_insert. by rewrite Closed_subst_p_id.
+    + by rewrite lookup_insert_ne.
+  - f_equal. simplify_option_eq.
+    + destruct_and!. 
+      rewrite !delete_insert_ne_binder' //.
+    + apply not_and_l in H as [<-%dec_stable|<-%dec_stable].
+      * rewrite delete_commute_binder.
+        cbn[delete delete_binder].
+        rewrite delete_insert_delete.
         rewrite (delete_commute_binder _ x0 (BNamed x)).
-        rewrite IHe. 
-        by rewrite (delete_commute_binder _ f (BNamed x)).
-      + apply not_and_l in H0 as [<-%dec_stable|<-%dec_stable].
-        * rewrite (delete_commute_binder _ x0 (BNamed x)).
-          by rewrite delete_delete.
-        * by rewrite delete_delete.
-  Qed.
+        reflexivity.
+      * cbn[delete delete_binder].
+        rewrite delete_insert_delete.
+        reflexivity.
+Qed.
   
-  Lemma subst_p_rec (x1 x2 : binder) v1 v2 e :
-    subst_p (<[x1:=v1]>{[x2:=v2]}) e = subst' x2 (of_val v2) (subst' x1 (of_val v1) e).
-  Proof.
-    replace (<[x1:=v1]> {[x2 := v2]})
-    with (<[x1:=v1]>(<[x2 := v2]>∅)); last first.
-    { destruct x1,x2; cbn; eauto. }
-    rewrite !subst_p_insert.
-    by rewrite subst_p_empty.
-  Qed.
+Lemma subst_p_delete (x : binder) (e' : expr) (m : stringmap val) e `{Closed ∅ e'} :
+  subst_p m (subst' x e' e) =
+  subst' x e' (subst_p (delete x m) e).
+Proof.
+  generalize dependent m.
+  destruct x as [|x]; cbn; auto.
+  induction e; simpl; intro m; auto 10 with f_equal;
+  repeat match goal with
+  | [ IH : subst_p _ _ = subst' _ _ _  |- _ ] => 
+    rewrite IH; clear IH
+  end.
+  - simplify_option_eq.
+    + rewrite lookup_delete. 
+      rewrite Closed_subst_p_id. simpl. by rewrite decide_left.
+    + rewrite lookup_delete_ne; auto.
+      case_match.
+      * by rewrite Closed_subst_id.
+      * simpl. by rewrite decide_False.
+  - f_equal. simplify_option_eq.
+    + destruct_and!. 
+      rewrite (delete_commute_binder _ x0 (BNamed x)).
+      rewrite IHe. 
+      by rewrite (delete_commute_binder _ f (BNamed x)).
+    + apply not_and_l in H0 as [<-%dec_stable|<-%dec_stable].
+      * rewrite (delete_commute_binder _ x0 (BNamed x)).
+        by rewrite delete_idem_binder.
+      * by rewrite delete_idem_binder.
+Qed.
+  
+Lemma subst_p_rec (x1 x2 : binder) v1 v2 e :
+  subst_p (<[x1:=v1]>{[x2:=v2]}) e = subst' x2 (of_val v2) (subst' x1 (of_val v1) e).
+Proof.
+  replace (<[x1:=v1]> {[x2 := v2]})
+  with (<[x1:=v1]>(<[x2 := v2]>∅)); last first.
+  { destruct x1,x2; cbn; eauto. }
+  rewrite !subst_p_insert.
+  by rewrite subst_p_empty.
+Qed.
 
   (* Other derived properties *)
   Lemma of_val_subst (v : val) x (es : expr) :
@@ -513,25 +385,25 @@ Admitted.
     by apply Closed_subst_id.
   Qed.
 
-  Lemma of_val_subst_p (v : val) (es : stringmap val) :
-    subst_p es (of_val v) = of_val v.
-  Proof.
-    by apply Closed_subst_p_id.
-  Qed.
-  
-  Lemma fill_item_subst_p (es : stringmap val) (Ki : ectx_item) (e : expr)  :
-    subst_p es (fill_item Ki e) = fill_item (subst_ctx_item es Ki) (subst_p es e).
-  Proof.
-    induction Ki; simpl;
-    rewrite ?of_val_subst_p; eauto.
-  Qed.
+Lemma of_val_subst_p (v : val) (es : stringmap val) :
+  subst_p es (of_val v) = of_val v.
+Proof.
+  by apply Closed_subst_p_id.
+Qed.
 
-  Lemma fill_subst (es : stringmap val) (K : list ectx_item) (e : expr) :
-    subst_p es (fill K e) = fill (subst_ctx es K) (subst_p es e).
-  Proof.
-    generalize dependent e. generalize dependent es.
-    induction K as [|Ki K]; eauto.
-    intros es e. simpl.
-    rewrite IHK.
-      by rewrite ?fill_item_subst_p.
-  Qed.
+Lemma fill_item_subst_p (es : stringmap val) (Ki : ectx_item) (e : expr)  :
+  subst_p es (fill_item Ki e) = fill_item (subst_ctx_item es Ki) (subst_p es e).
+Proof.
+  induction Ki; simpl;
+  rewrite ?of_val_subst_p; eauto.
+Qed.
+
+Lemma fill_subst (es : stringmap val) (K : list ectx_item) (e : expr) :
+  subst_p es (fill K e) = fill (subst_ctx es K) (subst_p es e).
+Proof.
+  generalize dependent e. generalize dependent es.
+  induction K as [|Ki K]; eauto.
+  intros es e. simpl.
+  rewrite IHK.
+    by rewrite ?fill_item_subst_p.
+Qed.
diff --git a/F_mu_ref_conc/typing.v b/F_mu_ref_conc/typing.v
index fd98365880f43e0c3f8601a6cab649ce58b23e8e..ba0e3b1cfd16c21484eb8af0d389462f1f6bd4bb 100644
--- a/F_mu_ref_conc/typing.v
+++ b/F_mu_ref_conc/typing.v
@@ -1,6 +1,6 @@
 From iris_logrel.F_mu_ref_conc Require Export lang notation subst.
 From iris_logrel.prelude Require Export base.
-From stdpp Require Export stringmap gmap mapset.
+From Autosubst Require Import Autosubst_Classes. (* for [subst] *)
 
 Inductive type :=
   | TUnit : type
@@ -88,71 +88,6 @@ Definition env_subst := subst_p.
 Lemma env_subst_empty (e : expr) : env_subst ∅ e = e.
 Proof. exact: subst_p_empty. Qed.
 
-(* (* TODO: FUNCTIONAL EXTENSIONALITY *) *)
-(* Require Import Coq.Logic.FunctionalExtensionality. *)
-(* Lemma env_subst_add (e : expr) (x : string) (v : val) vs : *)
-(*   vs !! x = None → *)
-(*   env_subst (<[x:=v]>vs) e = lang.subst x (of_val v) (env_subst vs e). *)
-(* Proof. cbv[env_subst]. intros ?. *)
-(*   rewrite map_fold_insert. reflexivity. *)
-(*   intros j1 j2 z1 z2 f Hj Hz1 Hz2. *)
-(*   apply functional_extensionality. *)
-(*   intro f0. apply subst_subst_ne; eauto. *)
-(*   apply H. *)
-(* Qed. *)
-
-(* Lemma env_subst_commute_3 (g : expr → expr → expr → expr) (vs : stringmap val) : *)
-(*   (∀ e1 e2 e3 x v, lang.subst x v (g e1 e2 e3) = g (lang.subst x v e1) (lang.subst x v e2) (lang.subst x v e3)) →  *)
-(*   forall e1 e2 e3, env_subst vs (g e1 e2 e3) = g (env_subst vs e1) (env_subst vs e2) (env_subst vs e3). *)
-(* Proof. *)
-(*   intros Hcomm e1 e2 e3. *)
-(*   pose (P:=(λ (_ : expr → expr) vs, env_subst vs (g e1 e2 e3) = g (env_subst vs e1) (env_subst vs e2) (env_subst vs e3))). *)
-(*   apply (map_fold_ind P (λ _ _, id) id); unfold P; simpl. *)
-(*   - by rewrite ?env_subst_empty. *)
-(*   - intros i vv m _ Hi IH. rewrite ?env_subst_add; auto. *)
-(*     rewrite IH. apply Hcomm. *)
-(* Qed.     *)
-
-(* Lemma env_subst_commute_2 (g : expr → expr → expr) (vs : stringmap val) : *)
-(*   (∀ e1 e2 x v, lang.subst x v (g e1 e2) = g (lang.subst x v e1) (lang.subst x v e2)) →  *)
-(*   forall e1 e2, env_subst vs (g e1 e2) = g (env_subst vs e1) (env_subst vs e2). *)
-(* Proof. *)
-(*   intros Hcomm e1 e2. *)
-(*   pose (P:=(λ (_ : expr → expr) vs, env_subst vs (g e1 e2) = g (env_subst vs e1) (env_subst vs e2))). *)
-(*   apply (map_fold_ind P (λ _ _, id) id); unfold P; simpl. *)
-(*   - by rewrite ?env_subst_empty. *)
-(*   - intros i vv m _ Hi IH. rewrite ?env_subst_add; auto. *)
-(*     rewrite IH. apply Hcomm. *)
-(* Qed.     *)
-
-(* Lemma env_subst_commute_1 (f : expr → expr) (vs : stringmap val) : *)
-(*   (∀ e x v, lang.subst x v (f e) = f (lang.subst x v e)) →  *)
-(*   forall e, env_subst vs (f e) = f (env_subst vs e). *)
-(* Proof. *)
-(*   intros Hcomm e.   *)
-(*   pose (P:=(λ (_ : expr → expr) m, env_subst m (f e) = f (env_subst m e))). *)
-(*   apply (map_fold_ind P (λ _ _, id) id); unfold P; simpl. *)
-(*   - by rewrite ?env_subst_empty. *)
-(*   - intros i vv m _ Hi IH. rewrite ?env_subst_add; auto. *)
-(*     rewrite IH. apply Hcomm. *)
-(* Qed.     *)
-
-(* Lemma env_subst_commute_0 (e : expr) (vs : stringmap val) : *)
-(*   (∀ x v, lang.subst x v e = e) → *)
-(*   env_subst vs e = e. *)
-(* Proof. *)
-(*   intros Hcomm.   *)
-(*   pose (P:=(λ (_ : expr → expr) m, env_subst m e = e)). *)
-(*   apply (map_fold_ind P (λ _ _, id) id); unfold P; simpl. *)
-(*   - by rewrite ?env_subst_empty. *)
-(*   - intros i vv m _ Hi IH. rewrite ?env_subst_add; auto. *)
-(*     rewrite IH. apply Hcomm. *)
-(* Qed. *)
-
-(* Lemma env_subst_of_val (v : val) (vs : stringmap val) : *)
-(*   env_subst vs (of_val v) = of_val v. *)
-(* Proof. apply subst_p_closed_empty. eapply val_closed. Qed. *)
-
 Lemma env_subst_lookup_None (vs : stringmap val) (x : string) :
   vs !! x = None →
    env_subst vs (Var x) = Var x.
diff --git a/_CoqProject b/_CoqProject
index a77aa722ee56827f91d7752053af2744c024ee50..6324d54a410a7a69e68c8326e1437194c8b807ab 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,6 @@
 -Q . iris_logrel
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+prelude/ds.v
 prelude/base.v
 F_mu_ref_conc/binder.v
 F_mu_ref_conc/lang.v
diff --git a/prelude/base.v b/prelude/base.v
index 92003750d43204facf18f8234be581eb58bddffe..758a434d9fa411a2d3d1a61e8a445266c17ea1e2 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -2,6 +2,7 @@ From iris.algebra Require Export base.
 From iris.base_logic Require Import upred.
 From iris.program_logic Require Import weakestpre.
 From iris.base_logic Require Import invariants.
+From iris_logrel.prelude Require Export ds.
 From Autosubst Require Export Autosubst.
 Import uPred.
 
diff --git a/prelude/ds.v b/prelude/ds.v
new file mode 100644
index 0000000000000000000000000000000000000000..03a042e6ca8bba5bbc401f9c57e2e3e607fb6edd
--- /dev/null
+++ b/prelude/ds.v
@@ -0,0 +1,66 @@
+(* Data structures properties *)
+(* TODO: move this to std++   *)
+From stdpp Require Export strings gmap mapset stringmap.
+From iris.algebra Require Export base. (* for ssreflect stuff *)
+
+Lemma delete_insert_delete {A} (m : stringmap A) (i : string) (x : A) :
+  delete i (<[i:=x]> m) = delete i m.
+Proof.
+  apply map_eq=>j.
+  destruct (decide (i = j)) as [Eij|Nij];
+    simplify_map_eq; auto.
+Qed.
+
+Lemma delete_idem {A} (x : string) (m : stringmap A) :
+  delete x (delete x m) = delete x m.
+Proof.
+  rewrite delete_notin; first done.
+  apply lookup_delete.
+Qed.
+
+Lemma delete_singleton_ne {A} (i j : string) (x : A) :
+  j ≠ i →
+  delete i {[j := x]} = {[j := x]}.
+Proof. intros Hij. apply delete_notin. by apply lookup_singleton_ne. Qed.
+
+Lemma difference_empty_map {K A} `{EqDecision K} `{Countable K} (X : gmap K A) :
+  X ∖ ∅ = X.
+Proof.
+  apply map_eq => i.
+  remember (X !! i) as Z. destruct Z.
+  - apply lookup_difference_Some. split; eauto.
+  - apply lookup_difference_None. left; eauto.
+Qed.
+
+Lemma singleton_union_difference (X Y : stringset) (x : string) :
+  {[x]} ∪ (X ∖ Y) = ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
+Proof.
+    unfold_leibniz. intros y. split; intro Hy. 
+    - apply elem_of_union in Hy. set_solver.
+    - apply elem_of_difference in Hy. destruct Hy as [Hy1 Hy2].
+      apply elem_of_union in Hy1.          
+      rewrite elem_of_union. rewrite elem_of_difference.
+      rewrite elem_of_singleton.
+      destruct (decide (x = y)); subst; eauto.
+      assert (y ∉ {[x]}). intro K; apply elem_of_singleton in K. auto.
+      right. destruct Hy1; set_solver.
+Qed.
+Lemma difference_union_id {A : Type} `{EqDecision A, Countable A} (X Y : gset A):
+  X ∖ Y ∪ Y = X ∪ Y.
+Proof.
+  unfold_leibniz. intro x.
+  rewrite !elem_of_union elem_of_difference.
+  split.
+  - set_solver.
+  - destruct (decide (x ∈ Y)); set_solver.
+Qed.
+Lemma difference_empty {A: Type} `{EqDecision A, Countable A} (X : gset A) :
+  X ∖ ∅ = X.
+Proof.
+  unfold_leibniz.
+  rewrite <- (right_id ∅ union (X ∖ ∅)).
+  rewrite <- (right_id ∅ union X) at 2.
+  fold_leibniz.
+  apply difference_union_id.
+Qed.
+