Clean up the repository

- Remove commented out code
- Pull std++ related lemmas into a separate file

F_mu_ref_conc/binder.v

 (* 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.

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') -∗

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) -∗

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' →

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.

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.

F_mu_ref_conc/subst.v

 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.