diff --git a/_CoqProject b/_CoqProject
index 04cd41783d35342d3d138ace27d59614743962ae..bc8bc716c57c4d11127a16ddd6fd39fc52747440 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -13,6 +13,7 @@ theories/logic/proofmode/tactics.v
 theories/typing/types.v
 theories/typing/interp.v
 theories/typing/fundamental.v
+theories/typing/contextual_refinement.v
 
 theories/tests/tp_tests.v
 theories/tests/proofmode_tests.v
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
new file mode 100644
index 0000000000000000000000000000000000000000..29b01950c42b5e46313204606090ffe16ccf7648
--- /dev/null
+++ b/theories/typing/contextual_refinement.v
@@ -0,0 +1,373 @@
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import tactics.
+From reloc.typing Require Export types interp fundamental.
+
+From Autosubst Require Import Autosubst.
+
+Inductive ctx_item :=
+  (* Î»-rec *)
+  | CTX_Rec (f x: binder)
+  | CTX_AppL (e2 : expr)
+  | CTX_AppR (e1 : expr)
+  (* Bin op *)
+  | CTX_BinOpL (op : bin_op) (e2 : expr)
+  | CTX_BinOpR (op : bin_op) (e1 : expr)
+  (* If *)
+  | CTX_IfL (e1 : expr) (e2 : expr)
+  | CTX_IfM (e0 : expr) (e2 : expr)
+  | CTX_IfR (e0 : expr) (e1 : expr)
+  (* Products *)
+  | CTX_PairL (e2 : expr)
+  | CTX_PairR (e1 : expr)
+  | CTX_Fst
+  | CTX_Snd
+  (* Sums *)
+  | CTX_InjL
+  | CTX_InjR
+  | CTX_CaseL (e1 : expr) (e2 : expr)
+  | CTX_CaseM (e0 : expr) (e2 : expr)
+  | CTX_CaseR (e0 : expr) (e1 : expr)
+  (* Recursive Types *)
+  | CTX_Fold
+  | CTX_Unfold
+  (* Polymorphic Types *)
+  | CTX_TLam
+  | CTX_TApp
+  (* Existential types *)
+  (* | CTX_Pack *)
+  (* | CTX_UnpackL (e' : expr) *)
+  (* | CTX_UnpackR (e : expr) *)
+  (* Concurrency *)
+  | CTX_Fork
+  (* Reference Types *)
+  | CTX_Alloc
+  | CTX_Load
+  | CTX_StoreL (e2 : expr)
+  | CTX_StoreR (e1 : expr)
+  (* Compare and swap used for fine-grained concurrency *)
+  | CTX_CAS_L (e1 : expr) (e2 : expr)
+  | CTX_CAS_M (e0 : expr) (e2 : expr)
+  | CTX_CAS_R (e0 : expr) (e1 : expr).
+
+Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
+  match ctx with
+  | CTX_Rec f x => Rec f x e
+  | CTX_AppL e2 => App e e2
+  | CTX_AppR e1 => App e1 e
+  | CTX_PairL e2 => Pair e e2
+  | CTX_PairR e1 => Pair e1 e
+  | CTX_Fst => Fst e
+  | CTX_Snd => Snd e
+  | CTX_InjL => InjL e
+  | CTX_InjR => InjR e
+  | CTX_CaseL e1 e2 => Case e e1 e2
+  | CTX_CaseM e0 e2 => Case e0 e e2
+  | CTX_CaseR e0 e1 => Case e0 e1 e
+  | CTX_BinOpL op e2 => BinOp op e e2
+  | CTX_BinOpR op e1 => BinOp op e1 e
+  | CTX_IfL e1 e2 => If e e1 e2
+  | CTX_IfM e0 e2 => If e0 e e2
+  | CTX_IfR e0 e1 => If e0 e1 e
+  | CTX_Fold => e
+  | CTX_Unfold => rec_unfold e
+  | CTX_TLam => Î›: e
+  | CTX_TApp => TApp e
+  (* | CTX_Pack => Pack e *)
+  (* | CTX_UnpackL e1 => Unpack e e1 *)
+  (* | CTX_UnpackR e0 => Unpack e0 e *)
+  | CTX_Fork => Fork e
+  | CTX_Alloc => Alloc e
+  | CTX_Load => Load e
+  | CTX_StoreL e2 => Store e e2
+  | CTX_StoreR e1 => Store e1 e
+  | CTX_CAS_L e1 e2 => CAS e e1 e2
+  | CTX_CAS_M e0 e2 => CAS e0 e e2
+  | CTX_CAS_R e0 e1 => CAS e0 e1 e
+  end.
+
+Definition ctx := list ctx_item.
+
+Definition fill_ctx (K : ctx) (e : expr) : expr := foldr fill_ctx_item e K.
+
+(** typed ctx *)
+Inductive typed_ctx_item :
+    ctx_item â†’ stringmap type â†’ type â†’ stringmap type â†’ type â†’ Prop :=
+  | TP_CTX_Rec Î“ Ï„ Ï„' f x :
+     typed_ctx_item (CTX_Rec f x) (<[f:=TArrow Ï„ Ï„']>(<[x:=Ï„]>Î“)) Ï„' Î“ (TArrow Ï„ Ï„')
+  | TP_CTX_AppL Î“ e2 Ï„ Ï„' :
+     typed Î“ e2 Ï„ â†’
+     typed_ctx_item (CTX_AppL e2) Î“ (TArrow Ï„ Ï„') Î“ Ï„'
+  | TP_CTX_AppR Î“ e1 Ï„ Ï„' :
+     typed Î“ e1 (TArrow Ï„ Ï„') â†’
+     typed_ctx_item (CTX_AppR e1) Î“ Ï„ Î“ Ï„'
+  | TP_CTX_PairL Î“ e2 Ï„ Ï„' :
+     typed Î“ e2 Ï„' â†’
+     typed_ctx_item (CTX_PairL e2) Î“ Ï„ Î“ (TProd Ï„ Ï„')
+  | TP_CTX_PairR Î“ e1 Ï„ Ï„' :
+     typed Î“ e1 Ï„ â†’
+     typed_ctx_item (CTX_PairR e1) Î“ Ï„' Î“ (TProd Ï„ Ï„')
+  | TP_CTX_Fst Î“ Ï„ Ï„' :
+     typed_ctx_item CTX_Fst Î“ (TProd Ï„ Ï„') Î“ Ï„
+  | TP_CTX_Snd Î“ Ï„ Ï„' :
+     typed_ctx_item CTX_Snd Î“ (TProd Ï„ Ï„') Î“ Ï„'
+  | TP_CTX_InjL Î“ Ï„ Ï„' :
+     typed_ctx_item CTX_InjL Î“ Ï„ Î“ (TSum Ï„ Ï„')
+  | TP_CTX_InjR Î“ Ï„ Ï„' :
+     typed_ctx_item CTX_InjR Î“ Ï„' Î“ (TSum Ï„ Ï„')
+  | TP_CTX_CaseL Î“ e1 e2 Ï„1 Ï„2 Ï„' :
+     typed Î“ e1 (TArrow Ï„1 Ï„') â†’ typed Î“ e2 (TArrow Ï„2 Ï„') â†’
+     typed_ctx_item (CTX_CaseL e1 e2) Î“ (TSum Ï„1 Ï„2) Î“ Ï„'
+  | TP_CTX_CaseM Î“ e0 e2 Ï„1 Ï„2 Ï„' :
+     typed Î“ e0 (TSum Ï„1 Ï„2) â†’ typed Î“ e2 (TArrow Ï„2 Ï„') â†’
+     typed_ctx_item (CTX_CaseM e0 e2) Î“ (TArrow Ï„1 Ï„') Î“ Ï„'
+  | TP_CTX_CaseR Î“ e0 e1 Ï„1 Ï„2 Ï„' :
+     typed Î“ e0 (TSum Ï„1 Ï„2) â†’ typed Î“ e1 (TArrow Ï„1 Ï„') â†’
+     typed_ctx_item (CTX_CaseR e0 e1) Î“ (TArrow Ï„2 Ï„') Î“ Ï„'
+  | TP_CTX_IfL Î“ e1 e2 Ï„ :
+     typed Î“ e1 Ï„ â†’ typed Î“ e2 Ï„ â†’
+     typed_ctx_item (CTX_IfL e1 e2) Î“ (TBool) Î“ Ï„
+  | TP_CTX_IfM Î“ e0 e2 Ï„ :
+     typed Î“ e0 (TBool) â†’ typed Î“ e2 Ï„ â†’
+     typed_ctx_item (CTX_IfM e0 e2) Î“ Ï„ Î“ Ï„
+  | TP_CTX_IfR Î“ e0 e1 Ï„ :
+     typed Î“ e0 (TBool) â†’ typed Î“ e1 Ï„ â†’
+     typed_ctx_item (CTX_IfR e0 e1) Î“ Ï„ Î“ Ï„
+  | TP_CTX_BinOpL_Nat op Î“ e2 Ï„ :
+     typed Î“ e2 TNat â†’
+     binop_nat_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpL op e2) Î“ TNat Î“ Ï„
+  | TP_CTX_BinOpR_Nat op e1 Î“ Ï„ :
+     typed Î“ e1 TNat â†’
+     binop_nat_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpR op e1) Î“ TNat Î“ Ï„
+  | TP_CTX_BinOpL_Bool op Î“ e2 Ï„ :
+     typed Î“ e2 TBool â†’
+     binop_bool_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpL op e2) Î“ TBool Î“ Ï„
+  | TP_CTX_BinOpR_Bool op e1 Î“ Ï„ :
+     typed Î“ e1 TBool â†’
+     binop_bool_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpR op e1) Î“ TBool Î“ Ï„
+  | TP_CTX_Fold Î“ Ï„ :
+     typed_ctx_item CTX_Fold Î“ Ï„.[(TRec Ï„)/] Î“ (TRec Ï„)
+  | TP_CTX_Unfold Î“ Ï„ :
+     typed_ctx_item CTX_Unfold Î“ (TRec Ï„) Î“ Ï„.[(TRec Ï„)/]
+  | TP_CTX_TLam Î“ Ï„ :
+     typed_ctx_item CTX_TLam (subst (ren (+1%nat)) <$> Î“) Ï„ Î“ (TForall Ï„)
+  | TP_CTX_TApp Î“ Ï„ Ï„' :
+     typed_ctx_item CTX_TApp Î“ (TForall Ï„) Î“ Ï„.[Ï„'/]
+  (* | TP_CTX_Pack Î“ Ï„ Ï„' : *)
+  (*    typed_ctx_item CTX_Pack Î“ Ï„.[Ï„'/] Î“ (TExists Ï„) *)
+  (* | TP_CTX_UnpackL e2 Î“ Ï„ Ï„2 : *)
+  (*    typed (subst (ren (+1)) <$> Î“) e2 (TArrow Ï„ (subst (ren (+1)) Ï„2)) â†’ *)
+  (*    typed_ctx_item (CTX_UnpackL e2) Î“ (TExists Ï„) Î“ Ï„2 *)
+  (* | TP_CTX_UnpackR e1 Î“ Ï„ Ï„2 : *)
+  (*    typed Î“ e1 (TExists Ï„) â†’ *)
+  (*    typed_ctx_item (CTX_UnpackR e1) (subst (ren (+1)) <$> Î“) (TArrow Ï„ (subst (ren (+1)) Ï„2))  Î“ Ï„2 *)
+  | TP_CTX_Fork Î“ :
+     typed_ctx_item CTX_Fork Î“ TUnit Î“ TUnit
+  | TPCTX_Alloc Î“ Ï„ :
+     typed_ctx_item CTX_Alloc Î“ Ï„ Î“ (Tref Ï„)
+  | TP_CTX_Load Î“ Ï„ :
+     typed_ctx_item CTX_Load Î“ (Tref Ï„) Î“ Ï„
+  | TP_CTX_StoreL Î“ e2 Ï„ :
+     typed Î“ e2 Ï„ â†’ typed_ctx_item (CTX_StoreL e2) Î“ (Tref Ï„) Î“ TUnit
+  | TP_CTX_StoreR Î“ e1 Ï„ :
+     typed Î“ e1 (Tref Ï„) â†’
+     typed_ctx_item (CTX_StoreR e1) Î“ Ï„ Î“ TUnit
+  | TP_CTX_CasL Î“ e1  e2 Ï„ :
+     EqType Ï„ â†’ UnboxedType Ï„ â†’
+     typed Î“ e1 Ï„ â†’ typed Î“ e2 Ï„ â†’
+     typed_ctx_item (CTX_CAS_L e1 e2) Î“ (Tref Ï„) Î“ TBool
+  | TP_CTX_CasM Î“ e0 e2 Ï„ :
+     EqType Ï„ â†’ UnboxedType Ï„ â†’
+     typed Î“ e0 (Tref Ï„) â†’ typed Î“ e2 Ï„ â†’
+     typed_ctx_item (CTX_CAS_M e0 e2) Î“ Ï„ Î“ TBool
+  | TP_CTX_CasR Î“ e0 e1 Ï„ :
+     EqType Ï„ â†’ UnboxedType Ï„ â†’
+     typed Î“ e0 (Tref Ï„) â†’ typed Î“ e1 Ï„ â†’
+     typed_ctx_item (CTX_CAS_R e0 e1) Î“ Ï„ Î“ TBool.
+
+Inductive typed_ctx: ctx â†’ stringmap type â†’ type â†’ stringmap type â†’ type â†’ Prop :=
+  | TPCTX_nil Î“ Ï„ :
+     typed_ctx nil Î“ Ï„ Î“ Ï„
+  | TPCTX_cons Î“1 Ï„1 Î“2 Ï„2 Î“3 Ï„3 k K :
+     typed_ctx_item k Î“2 Ï„2 Î“3 Ï„3 â†’
+     typed_ctx K Î“1 Ï„1 Î“2 Ï„2 â†’
+     typed_ctx (k :: K) Î“1 Ï„1 Î“3 Ï„3.
+
+(* Observable types are, at the moment, exactly the types which support equality. *)
+Definition ObsType : type â†’ Prop := EqType.
+
+Definition ctx_refines (Î“ : stringmap type)
+    (e e' : expr) (Ï„ : type) : Prop := âˆ€ K thp Ïƒâ‚€ Ïƒâ‚ v Ï„',
+  ObsType Ï„' â†’
+  typed_ctx K Î“ Ï„ âˆ… Ï„' â†’
+  rtc erased_step ([fill_ctx K e], Ïƒâ‚€) (of_val v :: thp, Ïƒâ‚) â†’
+  âˆƒ thp' Ïƒâ‚', rtc erased_step ([fill_ctx K e'], Ïƒâ‚€) (of_val v :: thp', Ïƒâ‚').
+Notation "Î“ âŠ¨ e 'â‰¤ctxâ‰¤' e' : Ï„" :=
+  (ctx_refines Î“ e e' Ï„) (at level 100, e, e' at next level, Ï„ at level 200).
+
+Lemma typed_ctx_item_typed k Î“ Ï„ Î“' Ï„' e :
+  typed Î“ e Ï„ â†’ typed_ctx_item k Î“ Ï„ Î“' Ï„' â†’
+  typed Î“' (fill_ctx_item k e) Ï„'.
+Proof. induction 2; simpl; eauto using typed. Qed.
+
+Lemma typed_ctx_typed K Î“ Ï„ Î“' Ï„' e :
+  typed Î“ e Ï„ â†’ typed_ctx K Î“ Ï„ Î“' Ï„' â†’ typed Î“' (fill_ctx K e) Ï„'.
+Proof. induction 2; simpl; eauto using typed_ctx_item_typed. Qed.
+
+Instance ctx_refines_reflexive Î“ Ï„ :
+  Reflexive (fun e1 e2 => ctx_refines Î“ e1 e2 Ï„).
+Proof.
+  intros e K thp ? Ïƒ v Ï„' HÏ„' Hty Hst.
+  eexists _,_. apply Hst.
+Qed.
+
+Instance ctx_refines_transitive Î“ Ï„ :
+  Transitive (fun e1 e2 => ctx_refines Î“ e1 e2 Ï„).
+Proof.
+  intros e1 e2 e3 Hctx1 Hctx2 K thp Ïƒâ‚€ Ïƒâ‚ v Ï„' HÏ„' Hty Hst.
+  destruct (Hctx1 K thp Ïƒâ‚€ Ïƒâ‚ v Ï„' HÏ„' Hty Hst) as [thp' [Ïƒ' Hst']].
+  by apply (Hctx2 K thp' _ Ïƒ' v Ï„' HÏ„').
+Qed.
+
+Lemma fill_ctx_app (K K' : ctx) (e : expr) :
+  fill_ctx K' (fill_ctx K e) = fill_ctx (K' ++ K) e.
+Proof. by rewrite /fill_ctx foldr_app. Qed.
+
+Lemma typed_ctx_compose (K K' : ctx) (Î“1 Î“2 Î“3 : stringmap type) (Ï„1 Ï„2 Ï„3 : type) :
+  typed_ctx K Î“1 Ï„1 Î“2 Ï„2 â†’
+  typed_ctx K' Î“2 Ï„2 Î“3 Ï„3 â†’
+  typed_ctx (K' ++ K) Î“1 Ï„1 Î“3 Ï„3.
+Proof.
+  revert Î“1 Î“2 Î“3 Ï„1 Ï„2 Ï„3.
+  induction K' as [|k K'] => Î“1 Î“2 Î“3 Ï„1 Ï„2 Ï„3.
+  - by inversion 2; simplify_eq/=.
+  - intros HK.
+    inversion 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]; simplify_eq/=.
+    specialize (IHK' _ _ _ _ _ _ HK Hx2).
+    econstructor; eauto.
+Qed.
+
+Lemma ctx_refines_congruence Î“ e1 e2 Ï„ Î“' Ï„' K :
+  typed_ctx K Î“ Ï„ Î“' Ï„' â†’
+  (Î“ âŠ¨ e1 â‰¤ctxâ‰¤ e2 : Ï„) â†’
+  Î“' âŠ¨ fill_ctx K e1 â‰¤ctxâ‰¤ fill_ctx K e2 : Ï„'.
+Proof.
+  intros HK Hctx K' thp Ïƒâ‚€ Ïƒâ‚ v Ï„'' HÏ„'' Hty.
+  rewrite !fill_ctx_app => Hst.
+  apply (Hctx (K' ++ K) thp Ïƒâ‚€ Ïƒâ‚ v Ï„'' HÏ„''); auto.
+  eapply typed_ctx_compose; eauto.
+Qed.
+
+Section bin_log_related_under_typed_ctx.
+  Context `{relocG Î£}.
+
+  (* Precongruence *)
+  Lemma bin_log_related_under_typed_ctx Î“ e e' Ï„ Î“' Ï„' K :
+    (typed_ctx K Î“ Ï„ Î“' Ï„') â†’
+    (â–¡ âˆ€ Î”, ({Î”;Î“} âŠ¨ e â‰¤logâ‰¤ e' : Ï„)) -âˆ—
+      (âˆ€ Î”, {Î”;Î“'} âŠ¨ fill_ctx K e â‰¤logâ‰¤ fill_ctx K e' : Ï„')%I.
+  Proof.
+    revert Î“ Ï„ Î“' Ï„' e e'.
+    induction K as [|k K]=> Î“ Ï„ Î“' Ï„' e e'; simpl.
+    - inversion_clear 1; trivial. iIntros "#H".
+      iIntros (Î”). by iApply "H".
+    - inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2].
+      specialize (IHK _ _ _ _ e e' Hx2).
+      inversion Hx1; subst; simpl; iIntros "#Hrel";
+        iIntros (Î”).
+      + iApply (bin_log_related_rec with "[-]"); auto.
+        iAlways. iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_app with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+        by iApply binary_fundamental.
+      + iApply (bin_log_related_app _ _ _ _ _ _ Ï„2 with "[]").
+        by iApply binary_fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_pair with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+        by iApply binary_fundamental.
+      + iApply (bin_log_related_pair with "[]").
+        by iApply binary_fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply bin_log_related_fst.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply bin_log_related_snd.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply bin_log_related_injl.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply bin_log_related_injr.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_case with "[] []").
+        iApply (IHK with "[Hrel]"); auto.
+        by iApply binary_fundamental.
+        by iApply binary_fundamental.
+      + iApply (bin_log_related_case with "[] []").
+        by iApply binary_fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+        by iApply binary_fundamental.
+      + iApply (bin_log_related_case with "[] []").
+        by iApply binary_fundamental.
+        by iApply binary_fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_if with "[] []");
+          try by iApply binary_fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_if with "[] []");
+          try by iApply binary_fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_if with "[] []");
+          try by iApply binary_fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_nat_binop with "[]");
+          try (by iApply binary_fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_nat_binop with "[]");
+          try (by iApply binary_fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_bool_binop with "[]");
+          try (by iApply binary_fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_bool_binop with "[]");
+          try (by iApply binary_fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_fold with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_unfold with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_tlam with "[]").
+        iIntros (Ï„i). iAlways.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_tapp' with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+      (* + iApply bin_log_related_pack'. *)
+      (*   iApply (IHK with "[Hrel]"); auto. *)
+      (* + iApply bin_log_related_unpack; try by (iIntros; fundamental). *)
+      (*   iApply (IHK with "[Hrel]"); auto. *)
+      (* + iApply bin_log_related_unpack; try by (iIntros; fundamental). *)
+      (*   iIntros. iApply (IHK with "[Hrel]"); auto. *)
+      + iApply (bin_log_related_fork with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_alloc with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_load with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_store with "[]");
+          try by iApply binary_fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_store with "[]");
+          try by iApply binary_fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_CAS with "[] []");
+          try (by iApply binary_fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_CAS with "[] []");
+          try (by iApply binary_fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_CAS with "[] []");
+          try (by iApply binary_fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+  Qed.
+End bin_log_related_under_typed_ctx.