diff --git a/F_mu_ref_conc/examples/counter.v b/F_mu_ref_conc/examples/counter.v
index 011cfa9df0a9de726a4dba7312fac9346ed29acf..26647867e5a0ef42210aa5e3c3e9b11cad3b71b1 100644
--- a/F_mu_ref_conc/examples/counter.v
+++ b/F_mu_ref_conc/examples/counter.v
@@ -401,8 +401,8 @@ Section CG_Counter.
     iApply (bin_log_related_rec_l _ ⊤ []); auto.
     iNext. simpl.
     rel_bind_r (App _ (#cnt')%E).
-    iApply (bin_log_related_rec_r _ _ ⊤ ); auto. simpl. rewrite !Closed_subst_id.
-    iApply (bin_log_related_rec_r _ [] ⊤); auto. simpl. rewrite !Closed_subst_id.
+    iApply (bin_log_related_rec_r _ _); auto. simpl. rewrite !Closed_subst_id.
+    iApply (bin_log_related_rec_r _ _ _ []); auto. simpl. rewrite !Closed_subst_id.
 
     unfold with_lock. unlock.
     rel_bind_r (App _ (λ: "l", _))%E.
@@ -411,7 +411,7 @@ Section CG_Counter.
     { simpl. by rewrite decide_left. }
     simpl. rewrite !Closed_subst_id.
 
-    iApply (bin_log_related_rec_r _ [] ⊤); eauto. simpl. rewrite !Closed_subst_id.
+    iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id.
 
     iApply bin_log_related_arrow. 
     iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
@@ -434,7 +434,7 @@ Section CG_Counter.
     (*   simpl. *)
     (*   iApply bin_log_related_unit. *)
     (*   Opaque CG_locked_increment with_lock. *)
-    iApply (bin_log_related_rec_r _ []); eauto. simpl. rewrite !Closed_subst_id.
+    iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id.
     iLöb as "IH".
     iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
     rel_bind_l (! #cnt)%E.
@@ -459,27 +459,27 @@ Section CG_Counter.
       rel_bind_r (acquire #l).
       iApply (bin_log_related_acquire_r with "Hl"); simpl; eauto. solve_ndisj. 
       iIntros "Hl".
-      iApply (bin_log_related_rec_r _ []); simpl; eauto. solve_ndisj.
+      iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto. solve_ndisj.
       rel_bind_r (App _ #())%E.
       iApply (bin_log_related_rec_r _ _); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id.
       rel_bind_r (CG_increment _ _).
       iApply (bin_log_related_CG_increment_r with "Hcnt'"). solve_ndisj. simpl.
       iIntros "Hcnt'".
-      iApply (bin_log_related_rec_r _ []); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id.
+      iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id.
       rel_bind_r (release #l)%E.
       iApply (bin_log_related_release_r with "Hl"). solve_ndisj.
       iIntros "Hl". simpl.
       iMod ("Hcl" with "[-]").
       { iNext. iExists _. by iFrame. }
       iApply (bin_log_related_if_true_l _ _ []). iNext. simpl.
-      iApply (bin_log_related_rec_r _ []); simpl; eauto.
+      iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto.
       iApply bin_log_related_unit.
     - (* CASE [m ≠ n], CAS fails *)
       iSplitL; last first. iIntros "%". exfalso. apply Hmn. by inversion H1.
       iIntros "% Hcnt". simpl.
       iMod ("Hcl" with "[-]").
       { iNext. iExists _. by iFrame. }
-      iApply (bin_log_related_if_false_l _ []). iNext. simpl.
+      iApply (bin_log_related_if_false_l _ _ []). iNext. simpl.
       iApply "IH".
   Qed.
 
@@ -490,7 +490,7 @@ Section CG_Counter.
     rel_bind_r newlock.
     iApply (bin_log_related_newlock_r); auto; simpl.
     iIntros (l) "Hl".
-    iApply (bin_log_related_rec_r _ []); auto. rewrite /= !Closed_subst_id /=.
+    iApply (bin_log_related_rec_r _ _ _ []); auto. rewrite /= !Closed_subst_id /=.
     rel_bind_l (Alloc _).
     iApply (bin_log_related_alloc_l); auto; simpl. iModIntro.
     iIntros (cnt) "Hcnt".        
@@ -507,19 +507,19 @@ Section CG_Counter.
     iApply (bin_log_related_rec_l _ _ []); auto.
     iNext. rewrite /= !Closed_subst_id /=.
 
-    iApply (bin_log_related_rec_r _ []); auto. simpl.
+    iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
     rewrite /= !Closed_subst_id /=.
     rel_bind_r (CG_counter_body _).    
     unfold CG_counter_body. unlock.
     iApply (bin_log_related_rec_r _ _); auto. 
     rewrite /= !Closed_subst_id /=.
-    iApply (bin_log_related_rec_r _ []); auto. 
+    iApply (bin_log_related_rec_r _ _ _ []); auto. 
     rewrite /= !Closed_subst_id /=.
     
     iApply (bin_log_related_pair _ with "[]"); last first.
     - Transparent counter_read.
       unfold counter_read. unlock.
-      iApply (bin_log_related_rec_r _ []); auto. simpl.
+      iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
       iApply (bin_log_related_rec_l _ _ []); auto. simpl. iNext.      
       iApply bin_log_related_rec; simpl. iAlways. cbn.
       iApply (bin_log_related_load_l _ _ _ []).
diff --git a/F_mu_ref_conc/relational_properties.v b/F_mu_ref_conc/relational_properties.v
index 83a5e59773a3914f9995b9ec8f4071b11c3abc05..d17fa3fe4385aacfce699bb7b94eddcfa4c4d32d 100644
--- a/F_mu_ref_conc/relational_properties.v
+++ b/F_mu_ref_conc/relational_properties.v
@@ -48,8 +48,9 @@ Section properties.
   Qed.
 
   (** ** Reductions on the left *)
-  (** Lifting of the pure reductions *)
-  Lemma bin_log_pure_l (Γ : stringmap type) (E : coPset) (τ : type) e e' t K'
+  (** *** Lifting of the pure reductions *)
+  Lemma bin_log_pure_l (Γ : stringmap type) (E : coPset) 
+    (K' : list ectx_item) (e e' t : expr) (τ : type)
     (Hclosed : Closed ∅ e)
     (Hclosed' : Closed ∅ e')
     (Hsafe : ∀ σ, head_reducible e σ) :
@@ -79,7 +80,8 @@ Section properties.
     iApply (fupd_mask_mono E); auto. 
   Qed.
 
-  Lemma bin_log_pure_masked_l Γ E1 E2 K' τ (e e' : expr) t
+  Lemma bin_log_pure_masked_l (Γ : stringmap type) (E1 E2 : coPset)
+    (K' : list ectx_item) (e e' t : expr) (τ : type)
     (Hclosed : Closed ∅ e)
     (Hclosed' : Closed ∅ e')
     (Hsafe : ∀ σ, head_reducible e σ) :
@@ -109,9 +111,9 @@ Section properties.
     done.
   Qed.
  
-  Lemma bin_log_related_fst_l Γ K e v1 v2 τ :
-   ▷ (Γ ⊨ (fill K (of_val v1)) ≤log≤ e : τ)
-   ⊢ Γ ⊨ (fill K (Fst (Pair (of_val v1) (of_val v2)))) ≤log≤ e : τ.
+  Lemma bin_log_related_fst_l Γ E K v1 v2 e τ :
+   ▷ ({E,E;Γ} ⊨ (fill K (of_val v1)) ≤log≤ e : τ)
+   ⊢ {E,E;Γ} ⊨ (fill K (Fst (Pair (of_val v1) (of_val v2)))) ≤log≤ e : τ.
   Proof.
     iIntros "Hlog".
     iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
@@ -119,9 +121,9 @@ Section properties.
     - by inversion H1.
   Qed.
 
-  Lemma bin_log_related_snd_l Γ K e v1 v2 τ :
-   ▷ (Γ ⊨ (fill K (of_val v2)) ≤log≤ e : τ)
-   ⊢ Γ ⊨ (fill K (Snd (Pair (of_val v1) (of_val v2)))) ≤log≤ e : τ.
+  Lemma bin_log_related_snd_l Γ E K v1 v2 e τ :
+   ▷ ({E,E;Γ} ⊨ (fill K (of_val v2)) ≤log≤ e : τ)
+   ⊢ {E,E;Γ} ⊨ (fill K (Snd (Pair (of_val v1) (of_val v2)))) ≤log≤ e : τ.
   Proof.
     iIntros "Hlog".
     iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
@@ -129,7 +131,7 @@ Section properties.
     - by inversion H1.
   Qed.
 
-  Lemma bin_log_related_rec_l Γ E K f x e e' v t τ
+  Lemma bin_log_related_rec_l Γ E K (f x : binder) e e' v t τ
    (Hclosed : Closed (x :b: f :b: ∅) e) :
    (to_val e' = Some v) →
    ▷ ({E,E;Γ} ⊨ (fill K (subst' f (Rec f x e) (subst' x e' e))) ≤log≤ t : τ)
@@ -152,10 +154,10 @@ Section properties.
       end. done.
   Qed.
 
-  Lemma bin_log_related_tlam_l Γ K e t τ
+  Lemma bin_log_related_tlam_l Γ E K e t τ
    (Hclosed : Closed ∅ e) :
-   ▷ (Γ ⊨ fill K e ≤log≤ t : τ)
-   ⊢ Γ ⊨ (fill K (TApp (TLam e))) ≤log≤ t : τ.
+   ▷ ({E,E;Γ} ⊨ fill K e ≤log≤ t : τ)
+   ⊢ {E,E;Γ} ⊨ (fill K (TApp (TLam e))) ≤log≤ t : τ.
   Proof.
     iIntros "Hlog".
     iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
@@ -165,11 +167,10 @@ Section properties.
       end. done.
   Qed.
 
-  Lemma bin_log_related_fold_l Γ K e v t τ
-   (Hclosed : Closed ∅ e) :
+  Lemma bin_log_related_fold_l Γ E K e v t τ :
    (to_val e = Some v) →
-   ▷ (Γ ⊨ fill K e ≤log≤ t : τ)
-   ⊢ Γ ⊨ (fill K (Unfold (Fold e))) ≤log≤ t : τ.
+   ▷ ({E,E;Γ} ⊨ fill K e ≤log≤ t : τ)
+   ⊢ {E,E;Γ} ⊨ (fill K (Unfold (Fold e))) ≤log≤ t : τ.
   Proof.
     iIntros (?) "Hlog".
     iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
@@ -179,12 +180,11 @@ Section properties.
       end. done.
   Qed.
   
-  Lemma bin_log_related_pack_l Γ K e e' v t τ
-   (Hclosed : Closed ∅ e) 
+  Lemma bin_log_related_pack_l Γ E K e e' v t τ
    (Hclosed' : Closed ∅ e') :
    (to_val e = Some v) →
-   ▷ (Γ ⊨ fill K (App e' e) ≤log≤ t : τ)
-   ⊢ Γ ⊨ (fill K (Unpack (Pack e) e')) ≤log≤ t : τ.
+   ▷ ({E,E;Γ} ⊨ fill K (App e' e) ≤log≤ t : τ)
+   ⊢ {E,E;Γ} ⊨ (fill K (Unpack (Pack e) e')) ≤log≤ t : τ.
   Proof.
     iIntros (?) "Hlog".
     iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
@@ -194,13 +194,12 @@ Section properties.
       end. done.
   Qed.
 
-  Lemma bin_log_related_case_inl_l Γ K e e1 e2 v t τ
-   (Hclosed : Closed ∅ e) 
+  Lemma bin_log_related_case_inl_l Γ E K e v e1 e2 t τ
    (Hclosed1 : Closed ∅ e1) 
    (Hclosed2 : Closed ∅ e2) : 
    (to_val e = Some v) →
-   ▷ (Γ ⊨ fill K (App e1 e) ≤log≤ t : τ)
-   ⊢ Γ ⊨ (fill K (Case (InjL e) e1 e2)) ≤log≤ t : τ.
+   ▷ ({E,E;Γ} ⊨ fill K (App e1 e) ≤log≤ t : τ)
+   ⊢ {E,E;Γ} ⊨ (fill K (Case (InjL e) e1 e2)) ≤log≤ t : τ.
   Proof.
     iIntros (?) "Hlog".
     iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
@@ -210,13 +209,12 @@ Section properties.
       end. done.
   Qed.
 
-  Lemma bin_log_related_case_inr_l Γ K e e1 e2 v t τ
-   (Hclosed : Closed ∅ e) 
+  Lemma bin_log_related_case_inr_l Γ E K e v e1 e2 t τ
    (Hclosed1 : Closed ∅ e1) 
    (Hclosed2 : Closed ∅ e2) : 
    (to_val e = Some v) →
-   ▷ (Γ ⊨ fill K (App e2 e) ≤log≤ t : τ)
-   ⊢ Γ ⊨ (fill K (Case (InjR e) e1 e2)) ≤log≤ t : τ.
+   ▷ ({E,E;Γ} ⊨ fill K (App e2 e) ≤log≤ t : τ)
+   ⊢ {E,E;Γ} ⊨ (fill K (Case (InjR e) e1 e2)) ≤log≤ t : τ.
   Proof.
     iIntros (?) "Hlog".
     iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
@@ -240,33 +238,33 @@ Section properties.
       end. done.
   Qed.
 
-  Lemma bin_log_related_if_false_l Γ K e1 e2 t τ
+  Lemma bin_log_related_if_true_masked_l Γ E1 E2 K e1 e2 t τ
    (Hclosed1 : Closed ∅ e1) 
    (Hclosed2 : Closed ∅ e2) : 
-   ▷ (Γ ⊨ fill K e2 ≤log≤ t : τ)
-   ⊢ Γ ⊨ (fill K (If (#♭ false) e1 e2)) ≤log≤ t : τ.
+   ({E1,E2;Γ} ⊨ fill K e1 ≤log≤ t : τ)
+   ⊢ {E1,E2;Γ} ⊨ (fill K (If (#♭ true) e1 e2)) ≤log≤ t : τ.
   Proof.
     iIntros "Hlog".
-    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
-    - do 3 eexists. econstructor; eauto.
-    - match goal with
-      | H : head_step _ _ _ _ _ |- _ => inversion H
-      end. done.
+    iApply (bin_log_pure_masked_l with "Hlog"); auto.
+    - do 3 eexists. econstructor; eauto. 
+    - by inversion 1.
   Qed.
 
-  Lemma bin_log_related_if_true_masked_l Γ E1 E2 (K : list ectx_item) (e1 e2 : expr) t τ
+  Lemma bin_log_related_if_false_l Γ E K e1 e2 t τ
    (Hclosed1 : Closed ∅ e1) 
    (Hclosed2 : Closed ∅ e2) : 
-   ({E1,E2;Γ} ⊨ fill K e1 ≤log≤ t : τ)
-   ⊢ {E1,E2;Γ} ⊨ (fill K (If (#♭ true) e1 e2)) ≤log≤ t : τ.
+   ▷ ({E,E;Γ} ⊨ fill K e2 ≤log≤ t : τ)
+   ⊢ {E,E;Γ} ⊨ (fill K (If (#♭ false) e1 e2)) ≤log≤ t : τ.
   Proof.
     iIntros "Hlog".
-    iApply (bin_log_pure_masked_l with "Hlog"); auto.
-    - do 3 eexists. econstructor; eauto. 
-    - by inversion 1.
+    iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
+    - do 3 eexists. econstructor; eauto.
+    - match goal with
+      | H : head_step _ _ _ _ _ |- _ => inversion H
+      end. done.
   Qed.
 
-  Lemma bin_log_related_if_false_masked_l Γ E1 E2 (K : list ectx_item) (e1 e2 : expr) t τ
+  Lemma bin_log_related_if_false_masked_l Γ E1 E2 K e1 e2 t τ
    (Hclosed1 : Closed ∅ e1) 
    (Hclosed2 : Closed ∅ e2) : 
    ({E1,E2;Γ} ⊨ fill K e2 ≤log≤ t : τ)
@@ -290,29 +288,29 @@ Section properties.
       end. done.
   Qed.
 
-  (** Stateful reductions *)
-  Lemma bin_log_related_step_l Φ K Γ E1 e1 e2 τ
+  (** *** Stateful reductions *)
+  Lemma bin_log_related_step_l Φ Γ E K e1 e2 τ
     (Hclosed1 : Closed ∅ e1) :
-    (|={E1}=> WP e1 @ E1 {{ Φ }}) -∗
-    (∀ v, Φ v -∗ {E1,E1;Γ} ⊨ fill K (of_val v) ≤log≤ e2 : τ) -∗
-    {E1,E1;Γ} ⊨ fill K e1 ≤log≤ e2 : τ.
+    (|={E}=> WP e1 @ E {{ Φ }}) -∗
+    (∀ v, Φ v -∗ {E,E;Γ} ⊨ fill K (of_val v) ≤log≤ e2 : τ) -∗
+    {E,E;Γ} ⊨ fill K e1 ≤log≤ e2 : τ.
   Proof.
     iIntros "He Hlog".
     iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=".
     rewrite /env_subst fill_subst /=.
     iApply (wp_bind (subst_ctx _ K)).    
     iMod "He". iModIntro.
-    iApply (wp_mask_mono E1); auto.
+    iApply (wp_mask_mono E); auto.
     rewrite Closed_subst_p_id.
     iApply (wp_wand with "He").
     iIntros (v) "Hv".
     iSpecialize ("Hlog" $! v with "Hv Hs [HΓ]"); first by iFrame.
     iSpecialize ("Hlog" with "Hj"). simpl.
     rewrite /env_subst fill_subst /=. rewrite of_val_subst_p.
-    iApply fupd_wp. iApply (fupd_mask_mono E1); auto.
+    iApply fupd_wp. iApply (fupd_mask_mono E); auto.
   Qed.
     
-  Lemma bin_log_related_wp_atomic_l K Γ (E1 E2 : coPset) e1 e2 τ
+  Lemma bin_log_related_wp_atomic_l Γ (E1 E2 : coPset) K e1 e2 τ
    (Hatomic : atomic e1)
    (Hclosed1 : Closed ∅ e1) :
    (|={E1,E2}=> WP e1 @ E2 {{ v,
@@ -335,7 +333,7 @@ Section properties.
     by iMod "Hlog".
   Qed.
   
-  Lemma bin_log_related_bind_l K Γ E e1 e2 τ
+  Lemma bin_log_related_bind_l Γ E K e1 e2 τ
    (Hclosed1 : Closed ∅ e1) :
    (WP e1 @ E {{ v,
      {E,E;Γ} ⊨ fill K (of_val v) ≤log≤ e2 : τ }})%I -∗
@@ -355,7 +353,7 @@ Section properties.
     done.
   Qed.
 
-  Lemma bin_log_related_step_atomic_l {A} (Φ : A → val → iProp Σ) K Γ E1 E2 e1 e2 τ
+  Lemma bin_log_related_step_atomic_l {A} (Φ : A → val → iProp Σ) Γ E1 E2 K e1 e2 τ
     (Hatomic : atomic e1)
     (Hclosed1 : Closed ∅ e1) :
     (|={E1,E2}=> ∃ (a : A), WP e1 @ E2 {{ v, Φ a v }} ∗
@@ -390,11 +388,11 @@ Section properties.
         end;
       try done.
 
-  Lemma bin_log_related_fork_l (Γ : stringmap type) K E1 (e t : expr) (τ : type)
+  Lemma bin_log_related_fork_l Γ E K (e t : expr) (τ : type)
    (Hclosed : Closed ∅ e) :
    ▷ (WP e {{ _, True }}) -∗
-   {E1,E1;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ -∗
-   {E1,E1;Γ} ⊨ fill K (Fork e) ≤log≤ t : τ.
+   {E,E;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ -∗
+   {E,E;Γ} ⊨ fill K (Fork e) ≤log≤ t : τ.
   Proof.
     iIntros "Hsafe Hlog".
     pose (Φ:=(fun w => ⌜w = UnitV⌝)%I : val -> iProp Σ).
@@ -425,7 +423,7 @@ Section properties.
       iApply ("Hlog" $! l with "Hl").
   Qed.
 
-  Lemma bin_log_related_alloc_l' Γ K E e v t τ
+  Lemma bin_log_related_alloc_l' Γ E K e v t τ
     (Heval : to_val e = Some v) :
     (∀ (l : loc), l ↦ᵢ v -∗ {E,E;Γ} ⊨ fill K (Loc l) ≤log≤ t : τ)%I
     -∗ {E,E;Γ} ⊨ fill K (Alloc e) ≤log≤ t : τ.
@@ -434,7 +432,7 @@ Section properties.
     iApply (bin_log_related_alloc_l); auto. assumption.
   Qed.
 
-  Lemma bin_log_related_load_l E1 E2 Γ K l t τ :
+  Lemma bin_log_related_load_l Γ E1 E2 K l t τ :
     (|={E1,E2}=> ∃ v',
       ▷(l ↦ᵢ v') ∗
       (l ↦ᵢ v' -∗ ({ E2,E1; Γ } ⊨ fill K (of_val v') ≤log≤ t : τ)))%I
@@ -453,7 +451,7 @@ Section properties.
       iApply "Hlog". done.
   Qed.
 
-  Lemma bin_log_related_load_l' Γ K E1 l v' t τ :
+  Lemma bin_log_related_load_l' Γ E1 K l v' t τ :
     ▷ (l ↦ᵢ v') -∗
     (l ↦ᵢ v' -∗ {E1,E1;Γ} ⊨ fill K (of_val v') ≤log≤ t : τ)
     -∗ {E1,E1;Γ} ⊨ fill K (Load (Loc l)) ≤log≤ t : τ.
@@ -465,7 +463,7 @@ Section properties.
     by iFrame.
   Qed.
 
-  Lemma bin_log_related_store_l Γ K E1 E2 l e v' t τ :
+  Lemma bin_log_related_store_l Γ E1 E2 K l e v' t τ :
     (to_val e = Some v') →
     (|={E1,E2}=> ∃ v, ▷ (l ↦ᵢ v) ∗
       (l ↦ᵢ v' -∗ {E2,E1;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ))
@@ -485,7 +483,7 @@ Section properties.
       iApply ("Hlog" with "Hl").
   Qed.
 
-  Lemma bin_log_related_store_l' Γ K E l e v v' t τ :
+  Lemma bin_log_related_store_l' Γ E K l e v v' t τ :
     (to_val e = Some v') →
     ▷ (l ↦ᵢ v) -∗
     (l ↦ᵢ v' -∗ {E,E;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ)
@@ -496,7 +494,7 @@ Section properties.
     iModIntro. iExists v. iFrame.
   Qed.
 
-  Lemma bin_log_related_cas_l Γ K E1 E2 l e1 e2 v1 v2 t τ :
+  Lemma bin_log_related_cas_l Γ E1 E2 K l e1 e2 v1 v2 t τ :
     (to_val e1 = Some v1) →
     (to_val e2 = Some v2) →
     (|={E1,E2}=> ∃ v', ▷ (l ↦ᵢ v') ∗ 
@@ -534,7 +532,7 @@ Section properties.
         iApply ("Hlog_fail" with "[] Hl"); auto.
   Qed.
 
-  Lemma bin_log_related_cas_fail_l Γ K E1 E2 l e1 e2 v1 v2 t τ :
+  Lemma bin_log_related_cas_fail_l Γ E1 E2 K l e1 e2 v1 v2 t τ :
     (to_val e1 = Some v1) →
     (to_val e2 = Some v2) →
     (|={E1,E2}=> ∃ v', ▷ (l ↦ᵢ v') ∗ ⌜v' ≠ v1⌝ ∗
@@ -555,7 +553,7 @@ Section properties.
       iApply ("Hlog" with "Hl").
   Qed.
   
-  Lemma bin_log_related_cas_fail_l' Γ K E l e1 e2 v1 v2 v' t τ :
+  Lemma bin_log_related_cas_fail_l' Γ E K l e1 e2 v1 v2 v' t τ :
     (to_val e1 = Some v1) →
     (to_val e2 = Some v2) →
     (v' ≠ v1) →
@@ -568,7 +566,7 @@ Section properties.
     iModIntro. iExists v'. iFrame "Hl Hlog". eauto.
   Qed.
 
-  Lemma bin_log_related_cas_suc_l Γ K E1 E2 l e1 e2 v1 v2 t τ :
+  Lemma bin_log_related_cas_suc_l Γ E1 E2 K l e1 e2 v1 v2 t τ :
     (to_val e1 = Some v1) →
     (to_val e2 = Some v2) →
     (|={E1,E2}=> ▷ (l ↦ᵢ v1) ∗
@@ -589,13 +587,13 @@ Section properties.
       iApply ("Hlog" with "Hl").
   Qed.
 
-  Lemma bin_log_related_cas_suc_l' Γ K l e1 e2 v1 v2 v' t τ :
+  Lemma bin_log_related_cas_suc_l' Γ E K l e1 e2 v1 v2 v' t τ :
     (to_val e1 = Some v1) →
     (to_val e2 = Some v2) →
     (v' = v1) →
     ▷ (l ↦ᵢ v') -∗
-    (l ↦ᵢ v2 -∗ Γ ⊨ fill K (#♭ true) ≤log≤ t : τ)
-    -∗ Γ ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ.
+    (l ↦ᵢ v2 -∗ {E,E;Γ} ⊨ fill K (#♭ true) ≤log≤ t : τ)
+    -∗ {E,E;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ.
   Proof.
     iIntros (???) "Hl Hlog". subst.
     iApply bin_log_related_cas_suc_l; eauto.
@@ -622,7 +620,7 @@ Section properties.
     iDestruct ("Hlog" with "Hs [HΓ] Hj") as "Hlog"; auto.    
   Qed.
 
-  Lemma bin_log_related_rec_r Γ K E1 E2 f x e e' t v' τ
+  Lemma bin_log_related_rec_r Γ E1 E2 K f x e e' t v' τ
    (Hspec : nclose specN ⊆ E1)
    (Hclosed : Closed (x :b: f :b: ∅) e) :
    (to_val e' = Some v') →
@@ -641,12 +639,41 @@ Section properties.
     { econstructor; eauto. }
   Qed.
 
-  (* TODO *)
-  (* Lemma bin_log_related_tlam_r Γ K e e' v' τ *)
-  (* Lemma bin_log_related_Fold_r Γ K e e' v' τ *)
-  (* Lemma bin_log_related_Pack_r Γ K e e' v' τ *)
+  Lemma bin_log_related_tlam_r Γ E1 E2 K e t τ
+   (Hclosed : Closed ∅ e)
+   (Hspec : nclose specN ⊆ E1) :
+   {E1,E2;Γ} ⊨ t ≤log≤ fill K e : τ
+   ⊢ {E1,E2;Γ} ⊨ t ≤log≤ fill K (TApp (TLam e)) : τ.
+  Proof.
+    iIntros "Hlog".
+    iApply (bin_log_pure_r with "Hlog"); auto; intros.
+    { econstructor; eauto. }
+  Qed.
+
+  Lemma bin_log_related_fold_r Γ E1 E2 K e v t τ
+   (Hval : to_val e = Some v)
+   (Hspec : nclose specN ⊆ E1) :
+   {E1,E2;Γ} ⊨ t ≤log≤ fill K e : τ
+   ⊢ {E1,E2;Γ} ⊨ t ≤log≤ fill K (Unfold (Fold e)) : τ.
+  Proof.
+    iIntros "Hlog".
+    iApply (bin_log_pure_r with "Hlog"); auto; intros.
+    { econstructor; eauto. }
+  Qed.
   
-  Lemma bin_log_related_fst_r Γ K E1 E2 e v1 v2 τ
+  Lemma bin_log_related_pack_r Γ E1 E2 K e e' v t τ
+   (Hclosed : Closed ∅ e')
+   (Hval : to_val e = Some v)
+   (Hspec : nclose specN ⊆ E1) :
+   {E1,E2;Γ} ⊨ t ≤log≤ fill K (App e' e) : τ
+   ⊢ {E1,E2;Γ} ⊨ t ≤log≤ fill K (Unpack (Pack e) e') : τ.
+  Proof.
+    iIntros "Hlog".
+    iApply (bin_log_pure_r with "Hlog"); auto; intros.
+    { econstructor; eauto. }
+  Qed.
+
+  Lemma bin_log_related_fst_r Γ E1 E2 K e v1 v2 τ
    (Hspec : nclose specN ⊆ E1) :
    {E1,E2;Γ} ⊨ e ≤log≤ (fill K (of_val v1)) : τ
    ⊢ {E1,E2;Γ} ⊨ e ≤log≤ (fill K (Fst (Pair (of_val v1) (of_val v2)))) : τ.
@@ -656,7 +683,7 @@ Section properties.
     { econstructor; eauto. }
   Qed.
 
-  Lemma bin_log_related_snd_r Γ K E1 E2 e v1 v2 τ
+  Lemma bin_log_related_snd_r Γ E1 E2 K e v1 v2 τ
    (Hspec : nclose specN ⊆ E1) :
    {E1,E2;Γ} ⊨ e ≤log≤ (fill K (of_val v2)) : τ
    ⊢ {E1,E2;Γ} ⊨ e ≤log≤ (fill K (Snd (Pair (of_val v1) (of_val v2)))) : τ.
@@ -666,9 +693,31 @@ Section properties.
     { econstructor; eauto. }
   Qed.
 
-  (* TODO *)
-  (* Lemma bin_log_related_inl_r Γ K e e' v' τ *)
-  (* Lemma bin_log_related_inr_r Γ K e e' v' τ *)
+  Lemma bin_log_related_inl_r Γ E1 E2 K e v e1 e2 t τ
+   (Hclosed1 : Closed ∅ e1) 
+   (Hclosed2 : Closed ∅ e2)   
+   (Hval : to_val e = Some v)
+   (Hspec : nclose specN ⊆ E1) :
+   {E1,E2;Γ} ⊨ t ≤log≤ (fill K (App e1 e)) : τ
+   ⊢ {E1,E2;Γ} ⊨ t ≤log≤ (fill K (Case (InjL e) e1 e2)) : τ.
+  Proof.
+    iIntros "Hlog".
+    iApply (bin_log_pure_r with "Hlog"); auto; intros.
+    { econstructor; eauto. }
+  Qed.
+
+  Lemma bin_log_related_inr_r Γ E1 E2 K e v e1 e2 t τ
+   (Hclosed1 : Closed ∅ e1) 
+   (Hclosed2 : Closed ∅ e2)   
+   (Hval : to_val e = Some v)
+   (Hspec : nclose specN ⊆ E1) :
+   {E1,E2;Γ} ⊨ t ≤log≤ (fill K (App e2 e)) : τ
+   ⊢ {E1,E2;Γ} ⊨ t ≤log≤ (fill K (Case (InjR e) e1 e2)) : τ.
+  Proof.
+    iIntros "Hlog".
+    iApply (bin_log_pure_r with "Hlog"); auto; intros.
+    { econstructor; eauto. }
+  Qed.
 
   Lemma bin_log_related_if_true_r Γ K E1 E2 e e1 e2 τ
    (Hspec : nclose specN ⊆ E1)