diff --git a/_CoqProject b/_CoqProject
index 4ddb0df66f40345a719eca4dc51f623f7be5571d..8cc2e1a3b7f4b63962c34fb47a5bfe9a77d4f806 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -25,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/prelude/lang_facts.v b/theories/prelude/lang_facts.v
index a6b05a3a050e046dec192e4890b4b0b1c4c688b0..7322a84c34d6fda15ebaa5eff6967545476cfd84 100644
--- a/theories/prelude/lang_facts.v
+++ b/theories/prelude/lang_facts.v
@@ -69,19 +69,22 @@ Section facts.
       simpl. by eapply erased_step_ectx.
   Qed.
 
-  Lemma nice_ctx_lemma K tp1 tp2 e ρ1 ρ2 v `{!LanguageCtx K} :
+  Lemma nice_ctx_lemma' K tp1 tp2 e ρ1 ρ2 v `{!LanguageCtx K} :
     rtc erased_step ρ1 ρ2 →
     ρ1.1 = (K e) :: tp1 →
     ρ2.1 = of_val v :: tp2 →
-    ∃ tp2' σ' w,
-      rtc erased_step (e :: tp1, ρ1.2) (of_val w :: tp2', σ').
+    ∃ 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 Hsteps.
     revert tp1 e.
     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 <-.
-      exists tp1, ρ.2, w. reflexivity.
+      - 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. }
@@ -89,31 +92,116 @@ Section facts.
     destruct t1 as [|h1 t1]; simplify_eq/=.
     - destruct (to_val e) as [w|] eqn:He.
       + apply of_to_val in He as <-.
-        eexists _, _, w. reflexivity.
+        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'&σ'&w&Hsteps1).
-        eexists _,_,w. eapply rtc_l, Hsteps1.
+        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'&σ'&w&Hsteps1).
-    eexists _,_,w. eapply rtc_l, Hsteps1.
+    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' σ' w,
-      rtc erased_step (e :: tp1, σ1) (of_val w :: tp2', σ').
+  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.
     pose (ρ1:=((K e) :: tp1, σ1)).
     pose (ρ2:=(of_val v :: tp2, σ2)).
     fold ρ1 ρ2. intros Hρ.
-    change σ1 with ρ1.2. eapply nice_ctx_lemma; eauto.
+    change σ1 with ρ1.2. eapply nice_ctx_lemma'; eauto.
   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 ϕ :
+    PureExec ϕ 1 e1 e2 →
+    ϕ →
+    rtc erased_step ρ1 ρ2 →
+    ρ1.1 = e1 :: tp1 →
+    ρ2.1 = of_val v :: tp2 →
+    rtc erased_step (e2 :: tp1, ρ1.2) ρ2.
+  Proof.
+    intros Hpure HÏ• Hsteps. revert tp1. 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.
+    intros ? ? ?.
+    pose (ρ1 := (e1 :: tp1, σ1)).
+    pose (ρ2 := (of_val v :: tp2, σ2)).
+    fold ρ1 ρ2. change σ1 with ρ1.2.
+    eapply pure_exec_inversion_lemma'; eauto.
+  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 10e7ddc5fc202af25fc111d85bbccdfba3cfc283..74980093bc13dfbabfa8a75f0d4a3cb03f9849e3 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -2,6 +2,7 @@
 (** 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.
@@ -241,16 +242,11 @@ 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 unboxed types
-which support direct equality tests. *)
-Definition ObsType : type → Prop := λ τ, EqType τ ∧ UnboxedType τ.
-
 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).
 
@@ -266,16 +262,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) :
@@ -301,64 +297,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.
 
-(* 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' (fill [AppRCtx (λ: <>, #true)]) []).
-    { apply _. }
-    eapply Hstep'.
-  - eapply (H C' thp _ σ1 #true TBool).
-    + repeat econstructor; eauto.
-    + 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.
-
 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 :
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/soundness.v b/theories/typing/soundness.v
index 150312044f9c1c8dec1ab6dfed9daffe9fd5cc0c..8be4cdef6afcca20304d4add8f100d27f2fe0c3e 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -4,6 +4,10 @@ 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' : τ) →
@@ -59,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 (? ?).