diff --git a/_CoqProject b/_CoqProject
index 43d2d0d90dbf645311eedf5156a4913c58e72e6b..8cc2e1a3b7f4b63962c34fb47a5bfe9a77d4f806 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -9,6 +9,7 @@ theories/prelude/ctx_subst.v
 theories/prelude/properness.v
 theories/prelude/asubst.v
 theories/prelude/bijections.v
+theories/prelude/lang_facts.v
 
 theories/logic/spec_ra.v
 theories/logic/spec_rules.v
@@ -24,6 +25,7 @@ theories/typing/types.v
 theories/typing/interp.v
 theories/typing/fundamental.v
 theories/typing/contextual_refinement.v
+theories/typing/contextual_refinement_alt.v
 theories/typing/tactics.v
 theories/typing/soundness.v
 
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 2cb61fb44de178a0582e657f130208acd7837d7a..3011969923459fe23d81d1d862df1a822c49cae3 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -124,5 +124,70 @@ Section compatibility.
     value_case.
   Qed.
 
+  Lemma refines_cmpxchg_ref A e1 e2 e3 e1' e2' e3' :
+    (REL e1 << e1' : lrel_ref (lrel_ref A)) -∗
+    (REL e2 << e2' : lrel_ref A) -∗
+    (REL e3 << e3' : lrel_ref A) -∗
+    REL (CmpXchg e1 e2 e3) << (CmpXchg e1' e2' e3') : lrel_prod (lrel_ref A) lrel_bool.
+  Proof.
+    iIntros "IH1 IH2 IH3".
+    rel_bind_l e3; rel_bind_r e3'.
+    iApply (refines_bind with "IH3").
+    iIntros (v3 v3') "#IH3".
+    rel_bind_l e2; rel_bind_r e2'.
+    iApply (refines_bind with "IH2").
+    iIntros (v2 v2') "#IH2".
+    rel_bind_l e1; rel_bind_r e1'.
+    iApply (refines_bind with "IH1").
+    iIntros (v1 v1') "#IH1 /=".
+    iPoseProof "IH1" as "IH1'".
+    iDestruct "IH1" as (l1 l2) "(% & % & Hinv)"; simplify_eq/=.
+    rewrite {2}/lrel_car /=.
+    iDestruct "IH2" as (r1 r2 -> ->) "Hr".
+    (* iDestruct "IH3" as (n1 n2 -> ->) "Hn". *)
+    rel_cmpxchg_l_atomic.
+    iInv (relocN .@ "ref" .@ (l1,l2)) as (v1 v2) "[Hl1 [>Hl2 #Hv]]" "Hclose".
+    iModIntro. iExists _; iFrame. simpl.
+    destruct (decide ((v1, v2) = (#r1, #r2))); simplify_eq/=.
+    - iSplitR; first by (iIntros (?); contradiction).
+      iIntros (?). iNext. iIntros "Hv1".
+      rel_cmpxchg_suc_r.
+      iMod ("Hclose" with "[-]").
+      { iNext. iExists _, _. by iFrame. }
+      rel_values. iExists _, _, _, _. do 2 (iSplitL; first done).
+      iFrame "Hv". iExists _. done.
+    - iSplit; iIntros (?); simplify_eq/=; iNext; iIntros "Hl1".
+      + destruct (decide (v2 = #r2)); simplify_eq/=.
+        * rewrite {5}/lrel_car. simpl.
+          iDestruct "Hv" as (r1' r2' ? ?) "#Hv". simplify_eq/=.
+          destruct (decide ((l1, l2) = (r1, r2'))); simplify_eq/=.
+          { iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(Hr1 & >Hr2 & Hrr)" "Hcl".
+            iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hl2") as %[]. }
+          destruct (decide ((l1, l2) = (r1', r2'))); simplify_eq/=.
+          ++ assert (r1' ≠ r1) by naive_solver.
+             iInv (relocN.@"ref".@(r1, r2')) as (? ?) "(Hr1 & >Hr2 & Hrr)" "Hcl".
+             iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hl2") as %[].
+          ++ iInv (relocN.@"ref".@(r1, r2')) as (? ?) "(Hr1 & >Hr2 & Hrr)" "Hcl".
+             iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(Hr1' & >Hr2' & Hrr')" "Hcl'".
+             iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hr2'") as %[].
+        * rel_cmpxchg_fail_r.
+          iMod ("Hclose" with "[-]").
+          { iNext; iExists _, _; by iFrame. }
+          rel_values. iModIntro. iExists _,_,_,_.
+          repeat iSplit; eauto.
+      + assert (v2 ≠ #r2) by naive_solver.
+        rewrite {5}/lrel_car. simpl.
+        iDestruct "Hv" as (r1' r2' ? ?) "#Hv". simplify_eq/=.
+        destruct (decide ((l1, l2) = (r1', r2'))); simplify_eq/=.
+        { iInv (relocN.@"ref".@(r1', r2)) as (? ?) "(>Hr1 & >Hr2 & Hrr)" "Hcl".
+          iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hl1") as %[]. }
+        destruct (decide ((l1, l2) = (r1', r2))); simplify_eq/=.
+        { iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(>Hr1 & >Hr2 & Hrr)" "Hcl".
+          iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hl1") as %[]. }
+        iInv (relocN.@"ref".@(r1', r2)) as (? ?) "(>Hr1 & >Hr2 & Hrr)" "Hcl".
+        iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(>Hr1' & >Hr2' & Hrr')" "Hcl'".
+        iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hr1'") as %[].
+  Qed.
+
 End compatibility.
 
diff --git a/theories/prelude/lang_facts.v b/theories/prelude/lang_facts.v
new file mode 100644
index 0000000000000000000000000000000000000000..4c4bbd68d61a87c7c643d0a3d1a2418308a0b71a
--- /dev/null
+++ b/theories/prelude/lang_facts.v
@@ -0,0 +1,197 @@
+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** Assorted facts about operational semantics. *)
+From iris.program_logic Require Import language.
+
+Section facts.
+  Context {Λ : language}.
+  Implicit Types e : expr Λ.
+  Implicit Types σ : state Λ.
+  Implicit Types tp : list (expr Λ).
+
+  Lemma erased_step_nonempty tp σ tp' σ'  :
+    erased_step (tp, σ) (tp', σ') → tp' ≠ [].
+  Proof.
+    intros [? Hs].
+    destruct Hs as [e1 σ1' e2 σ2' efs tp1 tp2 ?? Hstep]; simplify_eq/=.
+    intros [_ HH]%app_eq_nil. by inversion HH.
+  Qed.
+
+  Lemma rtc_erased_step_nonempty tp σ tp' σ'  :
+    rtc erased_step (tp, σ) (tp', σ') → tp ≠ [] → tp' ≠ [].
+  Proof.
+    pose (P := λ (x y : list (expr Λ) * (state Λ)), x.1 ≠ [] → y.1 ≠ []).
+    eapply (rtc_ind_r_weak P).
+    - intros [tp2 σ2]. unfold P. naive_solver.
+    - intros [tp1 σ1] [tp2 σ2] [tp3 σ3]. unfold P; simpl.
+      intros ? ?%erased_step_nonempty. naive_solver.
+  Qed.
+
+
+  Lemma erased_step_ectx e e' tp tp' σ σ' K `{!LanguageCtx K} :
+    erased_step (e :: tp, σ) (e' :: tp', σ') →
+    erased_step ((K e) :: tp, σ) (K e' :: tp', σ').
+  Proof.
+    intros [κ Hst]. inversion Hst; simplify_eq/=.
+    destruct t1 as [|h1 t1]; simplify_eq/=.
+    { simplify_eq/=.
+      eapply fill_step in H1. simpl in H1.
+      econstructor. eapply step_atomic with (t1 := []); eauto. }
+    econstructor. econstructor; eauto.
+    + rewrite app_comm_cons. reflexivity.
+    + rewrite app_comm_cons. reflexivity.
+  Qed.
+
+  Local Definition ffill K `{!LanguageCtx K} :
+    (list (expr Λ) * (state Λ)) → (list (expr Λ) * (state Λ)) :=
+    fun x => match x with
+             | (e :: tp, σ) => (K e :: tp, σ)
+             | ([], σ) => ([], σ)
+             end.
+
+  Lemma rtc_erased_step_ectx e e' tp tp' σ σ' K `{!LanguageCtx K} :
+    rtc erased_step (e :: tp, σ) (e' :: tp', σ') →
+    rtc erased_step (K e :: tp, σ) (K e' :: tp', σ').
+  Proof.
+    change (rtc erased_step (K e :: tp, σ) (K e' :: tp', σ'))
+      with (rtc erased_step (ffill K (e :: tp, σ)) (ffill K (e' :: tp', σ'))).
+    eapply (rtc_congruence (ffill K) erased_step).
+    clear e e' tp tp' σ σ'.
+    intros [tp σ] [tp' σ'].
+    destruct tp as [|e tp].
+    - inversion 1. inversion H0. exfalso.
+      simplify_eq/=. by eapply app_cons_not_nil.
+    - intros Hstep1.
+      assert (tp' ≠ []).
+      { eapply (rtc_erased_step_nonempty (e::tp)).
+        econstructor; naive_solver.
+        naive_solver. }
+      destruct tp' as [|e' tp']; first naive_solver.
+      simpl. by eapply erased_step_ectx.
+  Qed.
+
+  Lemma nice_ctx_lemma' K tp1 tp2 e ρ1 ρ2 v `{!LanguageCtx K} :
+    ρ1.1 = (K e) :: tp1 →
+    ρ2.1 = of_val v :: tp2 →
+    rtc erased_step ρ1 ρ2 →
+    ∃ tp2' tp3' σ' σ'' w,
+      rtc erased_step (e :: tp1, ρ1.2) (of_val w :: tp2', σ') ∧
+      rtc erased_step (K (of_val w) :: tp2', σ') (of_val v :: tp3', σ'').
+  Proof.
+    intros Heq1 Heq2 Hsteps.
+    revert tp1 e Heq1 Heq2.
+    induction Hsteps as [ρ|ρ1 ρ2 ρ3 Hstep Hsteps IH];
+      intros tp1 e Hρ1 Hρ2.
+    { destruct (to_val e) as [w|] eqn:He.
+      - apply of_to_val in He as <-.
+        destruct ρ as [ρ1 ρ2]. simplify_eq/=.
+        eexists _, _, _, _, w. split; first reflexivity.
+        rewrite H. reflexivity.
+    - assert (to_val (K e) = None) by auto using fill_not_val.
+      destruct ρ as [ρ1 ρ2]. simplify_eq/=.
+      assert (of_val v = K e) as ?%of_to_val_flip; naive_solver. }
+    destruct Hstep as [κs [e1 σ1 e2 σ2 efs t1 t2 -> -> Hstep]]; simpl in *.
+    destruct t1 as [|h1 t1]; simplify_eq/=.
+    - destruct (to_val e) as [w|] eqn:He.
+      + apply of_to_val in He as <-.
+        destruct ρ3 as [ρ3_1 ρ3_2]. simplify_eq/=.
+        eexists _, _, _, _, w. split; first reflexivity.
+        econstructor; last eassumption.
+        econstructor. eapply step_atomic with (t1:=[]); eauto.
+      + apply fill_step_inv in Hstep as (e2'&->&Hstep); last done.
+        specialize (IH (tp1++efs) e2').
+        assert (K e2' :: tp1 ++ efs = K e2' :: tp1 ++ efs) as H1 by done.
+        specialize (IH H1 Hρ2).
+        destruct IH as (tp2'&tp3'&σ'&σ''&w&[Hsteps1 Hsteps2]).
+        eexists _,_,_,_,w. split; last eassumption.
+        eapply rtc_l, Hsteps1.
+        exists κs. by eapply step_atomic with (t1:=[]).
+    - specialize (IH (t1 ++ e2 :: t2 ++ efs) e).
+      assert (K e :: t1 ++ e2 :: t2 ++ efs = K e :: t1 ++ e2 :: t2 ++ efs) as H1 by done.
+    specialize (IH H1 Hρ2).
+    destruct IH as (tp2'&tp3'&σ'&σ''&w&Hsteps1&Hstep2).
+    eexists _,_,_,_,w. split; last eassumption.
+    eapply rtc_l, Hsteps1.
+    exists κs. econstructor; rewrite ?app_comm_cons; done.
+  Qed.
+
+  Lemma nice_ctx_lemma K tp1 tp2 e σ1 σ2 v `{!LanguageCtx K} :
+    rtc erased_step (K e :: tp1, σ1) (of_val v :: tp2, σ2) →
+    ∃ tp2' tp3' σ' σ'' w,
+      rtc erased_step (e :: tp1, σ1) (of_val w :: tp2', σ') ∧
+      rtc erased_step (K (of_val w) :: tp2', σ') (of_val v :: tp3', σ'').
+  Proof. by eapply nice_ctx_lemma'. Qed.
+
+  Lemma nice_ctx_lemma_1 K tp1 tp2 e σ1 σ2 v `{!LanguageCtx K} :
+    rtc erased_step (K e :: tp1, σ1) (of_val v :: tp2, σ2) →
+    ∃ tp2' σ' w,
+      rtc erased_step (e :: tp1, σ1) (of_val w :: tp2', σ').
+  Proof.
+    intros Hρ.
+    cut (∃ tp2' tp3' σ' σ'' w,
+      rtc erased_step (e :: tp1, σ1) (of_val w :: tp2', σ') ∧
+      rtc erased_step (K (of_val w) :: tp2', σ') (of_val v :: tp3', σ'')).
+    { naive_solver. }
+    eapply nice_ctx_lemma; eauto.
+  Qed.
+
+  Local Ltac inv_step :=
+    match goal with
+    | [ H : erased_step _ _ |- _ ] => inversion H; clear H; simplify_eq/=; inv_step
+    | [ H : step _ _ _ |- _ ] => inversion H; clear H; simplify_eq/=
+    end.
+
+  Lemma pure_exec_inversion_lemma' tp1 tp2 e1 e2 ρ1 ρ2 v ϕ :
+    ρ1.1 = e1 :: tp1 →
+    ρ2.1 = of_val v :: tp2 →
+    PureExec ϕ 1 e1 e2 →
+    ϕ →
+    rtc erased_step ρ1 ρ2 →
+    rtc erased_step (e2 :: tp1, ρ1.2) ρ2.
+  Proof.
+    intros Heq1 Heq2 Hpure HÏ• Hsteps.
+    revert tp1 Heq1 Heq2. specialize (Hpure HÏ•).
+    apply nsteps_once_inv in Hpure.
+    revert e1 Hpure.
+    induction Hsteps as [ρ|ρ1 ρ2 ρ3 Hstep Hsteps IH]; intros e1 Hpure tp1 Hρ1 Hρ2.
+    - destruct ρ as [ρ_1 ρ_2]. simplify_eq/=.
+      assert (Inhabited (state Λ)).
+      { refine (populate ρ_2). }
+      assert (to_val e2 = Some v) as He2.
+      { by apply rtc_pure_step_val, rtc_once. }
+      apply of_to_val in He2. subst. naive_solver.
+    - destruct ρ1 as [? σ1].
+      destruct ρ2 as [tp σ2].
+      destruct ρ3 as [? σ3].
+      simplify_eq/=.
+      inv_step.
+      destruct t1 as [|h1 t1]; simplify_eq/=.
+      + eapply pure_step_det in H2; last done.
+        destruct_and!; simplify_eq/=. by rewrite app_nil_r in Hsteps.
+      + specialize (IH h1 Hpure (t1 ++ e3 :: t2 ++ efs) eq_refl eq_refl).
+        etrans; last by apply IH.
+        eapply rtc_once. econstructor.
+        eapply step_atomic with (t3:=(e2::t1)) (efs0:=efs); eauto.
+  Qed.
+
+  Lemma pure_exec_inversion_lemma tp1 tp2 e1 e2 σ1 σ2 v ϕ :
+    PureExec ϕ 1 e1 e2 →
+    ϕ →
+    rtc erased_step (e1 :: tp1, σ1) (of_val v :: tp2, σ2) →
+    rtc erased_step (e2 :: tp1, σ1) (of_val v :: tp2, σ2).
+  Proof. by eapply pure_exec_inversion_lemma'. Qed.
+
+  Lemma pure_exec_erased_step tp e1 e2 σ ϕ :
+    PureExec ϕ 1 e1 e2 →
+    ϕ →
+    erased_step (e1 :: tp, σ) (e2 :: tp, σ).
+  Proof.
+    intros Hpure HÏ•. specialize (Hpure HÏ•).
+    apply nsteps_once_inv in Hpure.
+    econstructor. eapply step_atomic with (t1:=[]) (efs:=[]); eauto.
+    { by rewrite app_nil_r. }
+    destruct (pure_step_safe _ _ Hpure σ) as (e2' & σ' & efs & Hstep).
+    destruct (pure_step_det _ _ Hpure _ _ _ _ _ Hstep).
+    naive_solver.
+  Qed.
+
+End facts.
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 7003acef7a029435eb99d98b2916851001d45a07..669627a6b0497c0ea984731c213dd00c3ad771cf 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -2,7 +2,9 @@
 (** Notion of contextual refinement & proof that it is a precongruence wrt the logical relation *)
 From Autosubst Require Import Autosubst.
 From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
+From reloc.prelude Require Import lang_facts.
 From reloc.typing Require Export types interp fundamental.
 
 Inductive ctx_item :=
@@ -138,12 +140,14 @@ Inductive typed_ctx_item :
      typed Γ e1 TBool →
      binop_bool_res_type op = Some τ →
      typed_ctx_item (CTX_BinOpR op e1) Γ TBool Γ τ
-  | TP_CTX_BinOpL_PtrEq e2 Γ τ :
-     typed Γ e2 (ref τ) →
-     typed_ctx_item (CTX_BinOpL EqOp e2) Γ (ref τ) Γ TBool
-  | TP_CTX_BinOpR_PtrEq e1 Γ τ :
-     typed Γ e1 (ref τ) →
-     typed_ctx_item (CTX_BinOpR EqOp e1) Γ (ref τ) Γ TBool
+  | TP_CTX_BinOpL_UnboxedEq e2 Γ τ :
+     UnboxedType τ →
+     typed Γ e2 τ →
+     typed_ctx_item (CTX_BinOpL EqOp e2) Γ τ Γ TBool
+  | TP_CTX_BinOpR_UnboxedEq e1 Γ τ :
+     UnboxedType τ →
+     typed Γ e1 τ →
+     typed_ctx_item (CTX_BinOpR EqOp e1) Γ τ Γ TBool
   | TP_CTX_IfL Γ e1 e2 τ :
      typed Γ e1 τ → typed Γ e2 τ →
      typed_ctx_item (CTX_IfL e1 e2) Γ (TBool) Γ τ
@@ -198,15 +202,15 @@ Inductive typed_ctx_item :
      Γ ⊢ₜ e1 : TRef TNat →
      typed_ctx_item (CTX_FAAR e1) Γ TNat Γ TNat
   | TP_CTX_CasL Γ e1 e2 τ :
-     EqType τ → UnboxedType τ →
+     UnboxedType τ →
      typed Γ e1 τ → typed Γ e2 τ →
      typed_ctx_item (CTX_CmpXchgL e1 e2) Γ (TRef τ) Γ (TProd τ TBool)
   | TP_CTX_CasM Γ e0 e2 τ :
-     EqType τ → UnboxedType τ →
+     UnboxedType τ →
      typed Γ e0 (TRef τ) → typed Γ e2 τ →
      typed_ctx_item (CTX_CmpXchgM e0 e2) Γ τ Γ (TProd τ TBool)
   | TP_CTX_CasR Γ e0 e1 τ :
-     EqType τ → UnboxedType τ →
+     UnboxedType τ →
      typed Γ e0 (TRef τ) → typed Γ e1 τ →
      typed_ctx_item (CTX_CmpXchgR e0 e1) Γ τ Γ (TProd τ TBool)
   (* Polymorphic & recursive types *)
@@ -238,15 +242,14 @@ Inductive typed_ctx: ctx → stringmap type → type → stringmap type → type
      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.
-
+(** The main definition of contextual refinement that we use. An
+    alternative (equivalent) formulation which observes only
+    termination can be found in [contextual_refinement_alt.v] *)
 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', σ₁').
+    (e e' : expr) (τ : type) : Prop := ∀ K thp σ₀ σ₁ (b : bool),
+  typed_ctx K Γ τ ∅ TBool →
+  rtc erased_step ([fill_ctx K e], σ₀) (of_val #b :: thp, σ₁) →
+  ∃ thp' σ₁', rtc erased_step ([fill_ctx K e'], σ₀) (of_val #b :: thp', σ₁').
 Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
   (ctx_refines Γ e e' τ) (at level 100, e, e' at next level, τ at level 200).
 
@@ -262,16 +265,16 @@ 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.
+  intros e K thp ? σ b 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τ').
+  intros e1 e2 e3 Hctx1 Hctx2 K thp σ₀ σ₁ b Hty Hst.
+  destruct (Hctx1 K thp σ₀ σ₁ b Hty Hst) as [thp' [σ' Hst']].
+  by apply (Hctx2 K thp' _ σ' b).
 Qed.
 
 Lemma fill_ctx_app (K K' : ctx) (e : expr) :
@@ -297,22 +300,20 @@ Lemma ctx_refines_congruence Γ e1 e2 τ Γ' τ' K :
   (Γ ⊨ e1 ≤ctx≤ e2 : τ) →
   Γ' ⊨ fill_ctx K e1 ≤ctx≤ fill_ctx K e2 : τ'.
 Proof.
-  intros HK Hctx K' thp σ₀ σ₁ v τ'' Hτ'' Hty.
+  intros HK Hctx K' thp σ₀ σ₁ v Hty.
   rewrite !fill_ctx_app => Hst.
-  apply (Hctx (K' ++ K) thp σ₀ σ₁ v τ'' Hτ''); auto.
+  apply (Hctx (K' ++ K) thp σ₀ σ₁ v); auto.
   eapply typed_ctx_compose; eauto.
 Qed.
 
-
 Definition ctx_equiv Γ e1 e2 τ :=
   (Γ ⊨ e1 ≤ctx≤ e2 : τ) ∧ (Γ ⊨ e2 ≤ctx≤ e1 : τ).
 
 Notation "Γ ⊨ e '=ctx=' e' : τ" :=
   (ctx_equiv Γ e e' τ) (at level 100, e, e' at next level, τ at level 200).
 
-
 Section bin_log_related_under_typed_ctx.
-  Context `{relocG Σ}.
+  Context `{!relocG Σ}.
 
   (* Precongruence *)
   Lemma bin_log_related_under_typed_ctx Γ e e' τ Γ' τ' K :
@@ -352,9 +353,9 @@ Section bin_log_related_under_typed_ctx.
       + iApply bin_log_related_bool_binop;
           try (by iApply fundamental); eauto.
         by iApply (IHK with "Hrel").
-      + iApply bin_log_related_ref_binop; try (by iApply fundamental).
+      + iApply bin_log_related_unboxed_eq; try (eassumption || by iApply fundamental).
         by iApply (IHK with "Hrel").
-      + iApply bin_log_related_ref_binop; try (by iApply fundamental).
+      + iApply bin_log_related_unboxed_eq; try (eassumption || by iApply fundamental).
         by iApply (IHK with "Hrel").
       + iApply (bin_log_related_if with "[] []");
           try by iApply fundamental.
diff --git a/theories/typing/contextual_refinement_alt.v b/theories/typing/contextual_refinement_alt.v
new file mode 100644
index 0000000000000000000000000000000000000000..c83d34434df58f8bbd8d9513bbfd9bd898677914
--- /dev/null
+++ b/theories/typing/contextual_refinement_alt.v
@@ -0,0 +1,148 @@
+From Autosubst Require Import Autosubst.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import tactics.
+From reloc.prelude Require Import lang_facts.
+From reloc.typing Require Export contextual_refinement.
+
+(* Alternative formulation of contextual refinement
+without restricting to contexts of the ground type *)
+Definition ctx_refines_alt (Γ : stringmap type)
+    (e e' : expr) (τ : type) : Prop := ∀ K thp σ₀ σ₁ v1 τ',
+  typed_ctx K Γ τ ∅ τ' →
+  rtc erased_step ([fill_ctx K e], σ₀) (of_val v1 :: thp, σ₁) →
+  ∃ thp' σ₁' v2, rtc erased_step ([fill_ctx K e'], σ₀) (of_val v2 :: thp', σ₁').
+
+
+Lemma ctx_refines_impl_alt Γ e1 e2 τ :
+  (Γ ⊨ e1 ≤ctx≤ e2 : τ) →
+  ctx_refines_alt Γ e1 e2 τ.
+Proof.
+  intros H C thp σ0 σ1 v1 τ' HC Hstep.
+  pose (C' := (CTX_AppR (λ: <>, #true)%E)::C).
+  cut (∃ (thp' : list expr) σ₁',
+              rtc erased_step ([fill_ctx C' e2], σ0)
+                (of_val #true :: thp', σ₁')).
+  - unfold C'; simpl.
+    destruct 1 as (thp' & σ1' & Hstep').
+    eapply (nice_ctx_lemma_1 (fill [AppRCtx (λ: <>, #true)]) []).
+    { apply _. }
+    eapply Hstep'.
+  - eapply (H C' thp _ σ1 true).
+    + repeat econstructor; eauto.
+    + unfold C'. simpl.
+      trans (((of_val v1) ;; #true)%E :: thp, σ1); last first.
+      { econstructor.
+        - econstructor.
+          eapply (step_atomic) with (t1 := []); try reflexivity.
+          eapply Ectx_step with (K:=[AppLCtx v1]); try reflexivity.
+          econstructor.
+        - eapply rtc_once. rewrite app_nil_r. econstructor.
+          eapply (step_atomic) with (efs:=[]) (t1 := []); try reflexivity.
+          { rewrite /= app_nil_r //. }
+          eapply Ectx_step with (K:=[]); try reflexivity.
+          by econstructor. }
+      pose (K := [AppRCtx (λ: <>, #true)%E]).
+      change (fill_ctx C e1;; #true)%E with (fill K (fill_ctx C e1)).
+      change (v1;; #true)%E with (fill K (of_val v1)).
+      by eapply rtc_erased_step_ectx; first by apply _.
+Qed.
+
+(* In order to prove the other direction we need a couple of auxiliary
+definitions *)
+
+Definition bot : val := rec: "bot" <> := "bot" #().
+Definition assert_ : val :=
+  λ: "v", if: "v" then #() else bot #().
+
+Local Ltac inv_step :=
+  match goal with
+  | [ H : erased_step _ _ |- _ ] => inversion H; clear H; simplify_eq/=; inv_step
+  | [ H : step _ _ _ |- _ ] => inversion H; clear H; simplify_eq/=
+  end.
+Local Ltac inv_rtc_step :=
+  match goal with
+  | [ H : rtc erased_step _ _ |- _ ] =>
+    inversion H as [|? [? ?] ? ?];
+    clear H; simplify_eq/=
+  end.
+Local Ltac solve_pure_exec :=
+  match goal with
+  | |- PureExec _ _ ?e1 _ =>
+    reshape_expr e1 ltac:(fun K e =>
+      eapply (pure_exec_ctx (fill K)); apply _)
+  end.
+
+Local Ltac side_cond_solver := unfold vals_compare_safe; naive_solver.
+
+Lemma rtc_erased_step_bot v tp1 tp2 σ1 σ2:
+  rtc erased_step (bot #() :: tp1, σ1) (of_val v :: tp2, σ2) →
+  False.
+Proof.
+  intros [n Hsteps]%rtc_nsteps. revert tp1 σ1 Hsteps.
+  induction (lt_wf n) as [n IH1 IH]=>tp1 σ1 Hsteps. destruct n as [|m].
+  - inversion Hsteps.
+  - inversion Hsteps; simplify_eq/=.
+    destruct y.
+    inv_step. destruct t1 as [|h1 t1]; simplify_eq/=.
+    + assert (PureExec True 1 (bot (of_val #())) (bot (of_val #()))).
+      { unfold bot.
+        assert (((rec: "bot" <> := "bot" #())%V #())
+                  = subst' <> #() (subst' "bot" bot ("bot" #()))) as HH.
+        { reflexivity. }
+        rewrite {2}HH. eapply pure_beta.
+        unfold bot. apply _. }
+      eapply pure_step_det in H3; last first.
+      { apply nsteps_once_inv. by eapply pure_exec. }
+      destruct_and!. simplify_eq/=.
+      eapply IH; eauto.
+    + eapply (IH m (lt_n_Sn m) (t1 ++ e2 :: t2 ++ efs)); eauto.
+Qed.
+
+Lemma ctx_refines_alt_impl Γ e1 e2 τ :
+  ctx_refines_alt Γ e1 e2 τ →
+  (Γ ⊨ e1 ≤ctx≤ e2 : τ).
+Proof.
+  intros Href C thp σ0 σ1 b HC Hstep.
+  pose (C' := [CTX_AppR (of_val assert_); CTX_BinOpL EqOp #b]).
+  assert (typed_ctx (C'++C) Γ τ ∅ TUnit) as Htyped.
+  { eapply typed_ctx_compose; eauto.
+    econstructor.
+    { econstructor. unfold assert_.
+      repeat econstructor; eauto. }
+    econstructor; last by econstructor.
+    econstructor; eauto. repeat econstructor; eauto. }
+  pose (K := [BinOpLCtx EqOp #b; AppRCtx assert_]).
+  assert (∃ thp' σ', rtc erased_step ([fill_ctx (C'++C) e1], σ0)
+              (of_val #() :: thp', σ')) as (thp1'&σ1'&Hassert1).
+  { simpl.
+    change (∃ (thp' : list expr) (σ' : state),
+               rtc erased_step ([fill K (fill_ctx C e1)], σ0) (of_val #() :: thp', σ')).
+    eexists _,_. trans (fill K (of_val #b) :: thp, σ1).
+    - eapply rtc_erased_step_ectx; eauto. apply _.
+    - simpl. econstructor.
+      + eapply pure_exec_erased_step ; [ solve_pure_exec | side_cond_solver ].
+      + simpl. rewrite bool_decide_eq_true_2 //.
+        econstructor.
+        * unfold assert_.
+          eapply pure_exec_erased_step ; [ solve_pure_exec | side_cond_solver ].
+        * simpl. eapply rtc_once.
+          eapply pure_exec_erased_step ; [ solve_pure_exec | naive_solver ]. }
+  assert (∃ thp' σ' v2, rtc erased_step ([fill_ctx (C'++C) e2], σ0)
+              (of_val v2 :: thp', σ')) as (thp2'&σ2'&v2&Hassert2).
+  { eapply Href; eauto. }
+  simpl in Hassert2.
+  destruct (nice_ctx_lemma (fill K) [] _ (fill_ctx C e2) σ0 _ v2 Hassert2)
+    as (tp2'&tp3'&σ3'&σ4'&w&Hw1&Hw2).
+  simpl in Hw2.
+  cut (w = #b); first by naive_solver.
+  revert Hw2. clear. intros Hw2.
+  eapply pure_exec_inversion_lemma in Hw2; [ | solve_pure_exec | side_cond_solver ].
+  simpl in Hw2. unfold assert_ in Hw2.
+  eapply pure_exec_inversion_lemma in Hw2; [ | solve_pure_exec | side_cond_solver ].
+  simpl in Hw2.
+  case_bool_decide; eauto. exfalso.
+  eapply pure_exec_inversion_lemma in Hw2; [ | solve_pure_exec | side_cond_solver ].
+  simpl in Hw2.
+  by eapply rtc_erased_step_bot.
+Qed.
+
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 87eefa61e53e20548eced215c1c6b95868078335..c51d82cb53cc0b3e5b82706ea4118b602b426fed 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -288,7 +288,7 @@ Section fundamental.
     rel_values.
   Qed.
 
-  Lemma bin_log_related_CmpXchg Δ Γ e1 e2 e3 e1' e2' e3' τ
+  Lemma bin_log_related_CmpXchg_EqType Δ Γ e1 e2 e3 e1' e2' e3' τ
     (HEqτ : EqType τ)
     (HUbτ : UnboxedType τ) :
     ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef τ) -∗
@@ -327,6 +327,24 @@ Section fundamental.
       iFrame "Hv". iExists _. done.
   Qed.
 
+  Lemma bin_log_related_CmpXchg Δ Γ e1 e2 e3 e1' e2' e3' τ
+    (HUbτ : UnboxedType τ) :
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef τ) -∗
+    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ) -∗
+    ({Δ;Γ} ⊨ e3 ≤log≤ e3' : τ) -∗
+    {Δ;Γ} ⊨ CmpXchg e1 e2 e3 ≤log≤ CmpXchg e1' e2' e3' : TProd τ TBool.
+  Proof.
+    cut (EqType τ ∨ ∃ τ', τ = TRef τ').
+    { intros [HÏ„ | [Ï„' ->]].
+      - by iApply bin_log_related_CmpXchg_EqType.
+      - iIntros "H1 H2 H3". intro_clause.
+        iSpecialize ("H1" with "Hvs").
+        iSpecialize ("H2" with "Hvs").
+        iSpecialize ("H3" with "Hvs").
+        iApply (refines_cmpxchg_ref with "H1 H2 H3"). }
+    by apply unboxed_type_ref_or_eqtype.
+  Qed.
+
   Lemma bin_log_related_alloc Δ Γ e e' τ :
     ({Δ;Γ} ⊨ e ≤log≤ e' : τ) -∗
     {Δ;Γ} ⊨ Alloc e ≤log≤ Alloc e' : TRef τ.
@@ -342,31 +360,25 @@ Section fundamental.
     rel_values. iExists l, k. eauto.
   Qed.
 
-  Lemma bin_log_related_ref_binop Δ Γ e1 e2 e1' e2' τ :
-    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef τ) -∗
-    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : TRef τ) -∗
+  Lemma bin_log_related_unboxed_eq Δ Γ e1 e2 e1' e2' τ :
+    UnboxedType τ →
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : τ) -∗
+    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ) -∗
     {Δ;Γ} ⊨ BinOp EqOp e1 e2 ≤log≤ BinOp EqOp e1' e2' : TBool.
   Proof.
-    iIntros "IH1 IH2".
+    iIntros (HÏ„) "IH1 IH2".
     intro_clause.
     rel_bind_ap e2 e2' "IH2" v2 v2' "#IH2".
     rel_bind_ap e1 e1' "IH1" v1 v1' "#IH1".
-    iDestruct "IH1" as (l1 l2) "[% [% #Hl]]"; simplify_eq/=.
-    iDestruct "IH2" as (l1' l2') "[% [% #Hl']]"; simplify_eq/=.
+    iAssert (⌜val_is_unboxed v1⌝)%I as "%".
+    { rewrite !unboxed_type_sound //.
+      iDestruct "IH1" as "[$ _]". }
+    iAssert (⌜val_is_unboxed v2'⌝)%I as "%".
+    { rewrite !unboxed_type_sound //.
+      iDestruct "IH2" as "[_ $]". }
+    iMod (unboxed_type_eq with "IH1 IH2") as "%"; first done.
     rel_op_l. rel_op_r.
-    destruct (decide (l1 = l1')) as [->|?].
-    - iMod (interp_ref_funct _ _ l1' l2 l2' with "[Hl Hl']") as %->.
-      { solve_ndisj. }
-      { iSplit; iExists _,_; eauto. }
-      rewrite !bool_decide_true //.
-      value_case.
-    - destruct (decide (l2 = l2')) as [->|?].
-      + iMod (interp_ref_inj _ _ l2' l1 l1' with "[Hl Hl']") as %->.
-        { solve_ndisj. }
-        { iSplit; iExists _,_; eauto. }
-        congruence.
-      + rewrite !bool_decide_false //; try congruence.
-        value_case.
+    do 2 case_bool_decide; first [by rel_values | naive_solver].
   Qed.
 
   Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' τ :
@@ -531,7 +543,7 @@ Section fundamental.
         by iApply fundamental.
       + iApply bin_log_related_bool_unop; first done.
         by iApply fundamental.
-      + iApply bin_log_related_ref_binop;
+      + iApply bin_log_related_unboxed_eq; try done;
           by iApply fundamental.
       + iApply bin_log_related_pair;
           by iApply fundamental.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 3f6e230b48e8f31a45c724174cb5c5ad3add8dc1..403a9ed0653aa879e30ea6133ae2134627991dbb 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -74,6 +74,35 @@ Section semtypes.
       + iDestruct "H1" as "[% [% H1]]"; simplify_eq/=.
         rewrite IHHÏ„2. by iDestruct "H1" as "%"; subst.
   Qed.
+
+  Lemma unboxed_type_eq τ Δ v1 v2 w1 w2 :
+    UnboxedType τ →
+    interp τ Δ v1 v2 -∗
+    interp τ Δ w1 w2 -∗
+    |={⊤}=> ⌜v1 = w1 ↔ v2 = w2⌝.
+  Proof.
+    intros Hunboxed.
+    cut (EqType τ ∨ ∃ τ', τ = TRef τ').
+    { intros [HÏ„ | [Ï„' ->]].
+      - rewrite !eq_type_sound //.
+        iIntros "% %". iModIntro.
+        iPureIntro. naive_solver.
+      - rewrite /lrel_car /=.
+        iDestruct 1 as (l1 l2 -> ->) "Hl".
+        iDestruct 1 as (r1 r2 -> ->) "Hr".
+        destruct (decide (l1 = r1)); subst.
+        + destruct (decide (l2 = r2)); subst; first by eauto.
+          iInv (relocN.@"ref".@(r1, l2)) as (v1 v2) "(>Hr1 & >Hr2 & Hinv1)".
+          iInv (relocN.@"ref".@(r1, r2)) as (w1 w2) "(>Hr1' & >Hr2' & Hinv2)".
+          iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hr1'") as %[].
+        + destruct (decide (l2 = r2)); subst; last first.
+          { iModIntro. iPureIntro. naive_solver. }
+          iInv (relocN.@"ref".@(r1, r2)) as (v1 v2) "(>Hr1 & >Hr2 & Hinv1)".
+          iInv (relocN.@"ref".@(l1, r2)) as (w1 w2) "(>Hr1' & >Hr2' & Hinv2)".
+          iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hr2'") as %[]. }
+    by apply unboxed_type_ref_or_eqtype.
+  Qed.
+
 End semtypes.
 
 (** ** Properties of the type inrpretation w.r.t. the substitutions *)
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 0e821dd6b8ff1ce2709600ff2f593cd56db8d42a..8be4cdef6afcca20304d4add8f100d27f2fe0c3e 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -4,11 +4,15 @@ From iris.proofmode Require Import tactics.
 From reloc.logic Require Export adequacy.
 From reloc.typing Require Export contextual_refinement.
 
+(* Observable types are, at the moment, exactly the unboxed types
+which support direct equality tests. *)
+Definition ObsType : type → Prop := λ τ, EqType τ ∧ UnboxedType τ.
+
 Lemma logrel_adequate Σ `{relocPreG Σ}
    e e' τ (σ : state) :
   (∀ `{relocG Σ} Δ, ⊢ {⊤;Δ;∅} ⊨ e ≤log≤ e' : τ) →
   adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h)
-    ∧ (ObsType τ → v = v')).
+    ∧ (EqType τ → v = v')).
 Proof.
   intros Hlog.
   set (A := λ (HΣ : relocG Σ), interp τ []).
@@ -20,7 +24,6 @@ Proof.
     { iApply env_ltyped2_empty. }
     by rewrite !fmap_empty !subst_map_empty.
   - intros HΣ v v'. unfold A. iIntros "Hvv".
-    unfold ObsType. cbn.
     iIntros (HÏ„). by iApply (eq_type_sound with "Hvv").
 Qed.
 
@@ -30,7 +33,7 @@ Theorem logrel_typesafety Σ `{relocPreG Σ} e e' τ thp σ σ' :
   not_stuck e' σ'.
 Proof.
   intros Hlog ??.
-  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e], σ) (of_val v' :: thp', h) ∧ (ObsType τ → v = v'))); first (intros [_ ?]; eauto).
+  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e], σ) (of_val v' :: thp', h) ∧ (EqType τ → v = v'))); first (intros [_ ?]; eauto).
   eapply logrel_adequate; eauto.
 Qed.
 
@@ -51,8 +54,8 @@ Lemma logrel_simul Σ `{relocPreG Σ}
   (∃ thp' hp' v', rtc erased_step ([e'], σ) (of_val v' :: thp', hp') ∧ (ObsType τ → v = v')).
 Proof.
   intros Hlog Hsteps.
-  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h) ∧ (ObsType τ → v = v'))).
-  { destruct 1; naive_solver. }
+  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h) ∧ (EqType τ → v = v'))).
+  { unfold ObsType. destruct 1; naive_solver. }
   eapply logrel_adequate; eauto.
 Qed.
 
@@ -60,8 +63,10 @@ Lemma refines_sound_open Σ `{relocPreG Σ} Γ e e' τ :
   (∀ `{relocG Σ} Δ, ⊢ {⊤;Δ;Γ} ⊨ e ≤log≤ e' : τ) →
   Γ ⊨ e ≤ctx≤ e' : τ.
 Proof.
-  intros Hlog K thp σ₀ σ₁ v τ' ? Htyped Hstep.
-  cut (∃ thp' hp' v', rtc erased_step ([fill_ctx K e'], σ₀) (of_val v' :: thp', hp') ∧ (ObsType τ'  → v = v')).
+  intros Hlog K thp σ₀ σ₁ b Htyped Hstep.
+  assert (ObsType TBool).
+  { repeat econstructor; eauto. }
+  cut (∃ thp' hp' v', rtc erased_step ([fill_ctx K e'], σ₀) (of_val v' :: thp', hp') ∧ (ObsType TBool  → #b = v')).
   { naive_solver. }
   eapply (logrel_simul Σ); last by apply Hstep.
   iIntros (? ?).
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 4c76bdb3ef867f7810b098c0b5cfbced6b6c728a..678eb6c8d373cc1baa3e0dd232a18f092677df5f 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -18,7 +18,15 @@ Inductive type :=
   | TExists : {bind 1 of type} → type
   | TRef : type → type.
 
-(** Which types support equality testing *)
+(** Which types are unboxed -- we can only do CAS on locations which hold unboxed types *)
+Inductive UnboxedType : type → Prop :=
+  | UnboxedTUnit : UnboxedType TUnit
+  | UnboxedTNat : UnboxedType TNat
+  | UnboxedTBool : UnboxedType TBool
+  | UnboxedTRef Ï„ : UnboxedType (TRef Ï„).
+
+(** Types which support direct equality test (which coincides with ctx equiv).
+    This is an auxiliary notion. *)
 Inductive EqType : type → Prop :=
   | EqTUnit : EqType TUnit
   | EqTNat : EqType TNat
@@ -26,12 +34,9 @@ Inductive EqType : type → Prop :=
   | EqTProd τ τ' : EqType τ → EqType τ' → EqType (TProd τ τ')
   | EqSum τ τ' : EqType τ → EqType τ' → EqType (TSum τ τ').
 
-(** Which types are unboxed -- we can only do CAS on locations which hold unboxed types *)
-Inductive UnboxedType : type → Prop :=
-  | UnboxedTUnit : UnboxedType TUnit
-  | UnboxedTNat : UnboxedType TNat
-  | UnboxedTBool : UnboxedType TBool
-  | UnboxedTRef Ï„ : UnboxedType (TRef Ï„).
+Lemma unboxed_type_ref_or_eqtype Ï„ :
+  UnboxedType τ → (EqType τ ∨ ∃ τ', τ = TRef τ').
+Proof. inversion 1; first [ left; by econstructor | right; naive_solver ]. Qed.
 
 (** Autosubst instances *)
 Instance Ids_type : Ids type. derive. Defined.
@@ -135,8 +140,9 @@ Inductive typed : stringmap type → expr → type → Prop :=
      Γ ⊢ₜ e : TBool →
      unop_bool_res_type op = Some τ →
      Γ ⊢ₜ UnOp op e : τ
-  | RefEq_typed Γ e1 e2 τ :
-     Γ ⊢ₜ e1 : ref τ → Γ ⊢ₜ e2 : ref τ →
+  | UnboxedEq_typed Γ e1 e2 τ :
+     UnboxedType τ →
+     Γ ⊢ₜ e1 : τ → Γ ⊢ₜ e2 : τ →
      Γ ⊢ₜ BinOp EqOp e1 e2 : TBool
   | Pair_typed Γ e1 e2 τ1 τ2 :
      Γ ⊢ₜ e1 : τ1 → Γ ⊢ₜ e2 : τ2 →
@@ -198,7 +204,7 @@ Inductive typed : stringmap type → expr → type → Prop :=
      Γ ⊢ₜ e2 : TNat →
      Γ ⊢ₜ FAA e1 e2 : TNat
   | TCmpXchg Γ e1 e2 e3 τ :
-     EqType τ → UnboxedType τ →
+     UnboxedType τ →
      Γ ⊢ₜ e1 : ref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
      Γ ⊢ₜ CmpXchg e1 e2 e3 : τ * TBool
 with val_typed : val → type → Prop :=