diff --git a/_CoqProject b/_CoqProject
index dbbad9920567b1a21ce16f6df11a72664cc30670..c5b6d1ac3e7f6d44f6b24726a4ee495f15b976ef 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -28,3 +28,4 @@ theories/tests/proofmode_tests.v
 
 theories/examples/lock.v
 theories/examples/counter.v
+theories/examples/bit.v
diff --git a/theories/examples/bit.v b/theories/examples/bit.v
new file mode 100644
index 0000000000000000000000000000000000000000..e1aea7718257996bbca30b113181e8ff01559053
--- /dev/null
+++ b/theories/examples/bit.v
@@ -0,0 +1,87 @@
+From iris.proofmode Require Import tactics.
+From reloc Require Import proofmode.
+From reloc.typing Require Import types interp fundamental.
+From reloc.typing Require Import soundness.
+
+(* TODO: these modules should be values -- but we don't have refines_pair for values *)
+Definition bit_bool : expr :=
+  (#true, (λ: "b", ~ "b"), (λ: "b", "b")).
+
+Definition flip_nat : val := λ: "n",
+  if: "n" = #0
+  then #1
+  else #0.
+Definition bit_nat : expr :=
+  (#1, flip_nat, (λ: "b", "b" = #1)).
+
+Definition bitτ : type :=
+  (TExists (TProd (TProd (TVar 0)
+                         (TArrow (TVar 0) (TVar 0)))
+                         (TArrow (TVar 0) (TBool))))%nat.
+
+
+Section bit_refinement.
+  Context `{relocG Σ}.
+
+  Definition bitf (b : bool) : nat :=
+    match b with
+    | true => 1
+    | false => 0
+    end.
+
+  (* This is the graph of the `bitf` function *)
+  Definition bitτi : lty2 Σ := Lty2 (λ v1 v2,
+    (∃ b : bool, ⌜v1 = #b⌝ ∗ ⌜v2 = #(bitf b)⌝))%I.
+
+  Lemma bit_refinement Δ :
+    REL bit_bool << bit_nat : (interp bitτ Δ).
+  Proof.
+    unfold bit_bool, bit_nat.
+    unfold bitτ. simpl.
+    iApply (refines_exists bitτi).
+    progress repeat iApply refines_pair.
+    - rel_values.
+    - unfold flip_nat. rel_pure_l. unlock. (* TODO: can we make the tactics do unlocking? *)
+      iApply refines_arrow_val.
+      iIntros "!#" (v1 v2) "/=".
+      iIntros ([b [? ?]]); simplify_eq/=.
+      repeat rel_pure_l. repeat rel_pure_r.
+      destruct b; simpl; rel_if_r; rel_values.
+    - rel_pure_l. rel_pure_r. unlock.
+      iApply refines_arrow_val.
+      iIntros "!#" (v1 v2) "/=".
+      iIntros ([b [? ?]]); simplify_eq/=.
+      repeat rel_pure_l. repeat rel_pure_r.
+      destruct b; simpl; rel_values.
+  Qed.
+
+End bit_refinement.
+
+Theorem bit_ctx_refinement :
+  ∅ ⊨ bit_bool ≤ctx≤ bit_nat : bitτ.
+Proof.
+  eapply (logrel_ctxequiv relocΣ).
+  iIntros (? ? vs) "Hvs". simpl.
+  (* TODO: this is not the place to have this boilerplate *)
+  rewrite !lookup_delete.
+  iApply (bit_refinement Δ).
+Qed.
+
+(* Definition heapify : val := λ: "b", Unpack "b" $ λ: "b'", *)
+(*   let: "init" := Fst (Fst "b'") in *)
+(*   let: "flip" := Snd (Fst "b'") in *)
+(*   let: "view" := Snd "b'" in *)
+(*   let: "x" := ref "init" in *)
+(*   let: "l" := newlock #() in *)
+(*   let: "flip_ref" := λ: <>, acquire "l";; "x" <- "flip" (!"x");; release "l" in *)
+(*   let: "view_ref" := λ: <>, "view" (!"x") in *)
+(*   (#(), "flip_ref", "view_ref"). *)
+
+(* Lemma heapify_type Γ : *)
+(*   typed Γ heapify (TArrow bitτ bitτ). *)
+(* Proof. *)
+(*   unfold bitτ. unfold heapify. *)
+(*   unlock. *)
+(*   repeat (econstructor; solve_typed). (* TODO: solve_typed does not work by itself :( *) *)
+(* Qed. *)
+(* Hint Resolve heapify_type : typeable. *)
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 941c0960a3b0e26ecd7c024ba02e47812dd916a3..e7b2bfdc49e8ff09684c88cdf282e7e132194d45 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -58,4 +58,15 @@ Section compatibility.
     - iExists #(); eauto.
   Qed.
 
+  Lemma refines_exists (A : lty2 Σ) e e' (C : lty2 Σ → lty2 Σ) :
+    (REL e << e' : C A) -∗
+    REL e << e' : ∃ A, C A.
+  Proof.
+    iIntros "H".
+    rel_bind_ap e e' "H" v v' "Hvv".
+    value_case.
+    iModIntro. iExists A. done.
+  Qed.
+
 End compatibility.
+
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 9c1a68135d60b95f3addaa3f5a82a04252936ba6..608098c3353c4aeb21ea4eb4fd79a5c62dc69c44 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -137,6 +137,8 @@ Notation "()" := lty2_unit : lty_scope.
 Infix "→" := lty2_arr : lty_scope.
 Infix "×" := lty2_prod (at level 80) : lty_scope.
 Notation "'ref' A" := (lty2_ref A) : lty_scope.
+Notation "∃ A1 .. An , C" :=
+  (lty2_exists (λ A1, .. (lty2_exists (λ An, C%lty2)) ..)) : lty_scope.
 
 Section refinement.
   Context `{relocG Σ}.