diff --git a/theories/logrel/F_mu_ref_conc/binary/context_refinement.v b/theories/logrel/F_mu_ref_conc/binary/context_refinement.v
index 89eb137cdc9cfbb78b638b955f11add0f6a0e7f0..d1d67255f0cf09c4205b5cc018fb44876d3c1d55 100644
--- a/theories/logrel/F_mu_ref_conc/binary/context_refinement.v
+++ b/theories/logrel/F_mu_ref_conc/binary/context_refinement.v
@@ -7,6 +7,11 @@ Export F_mu_ref_conc.
 
 Inductive ctx_item :=
   | CTX_Rec
+  | CTX_Lam
+  | CTX_LetInL (e2 : expr)
+  | CTX_LetInR (e1 : expr)
+  | CTX_SeqL (e2 : expr)
+  | CTX_SeqR (e1 : expr)
   | CTX_AppL (e2 : expr)
   | CTX_AppR (e1 : expr)
   (* Products *)
@@ -33,6 +38,10 @@ Inductive ctx_item :=
   (* Polymorphic Types *)
   | CTX_TLam
   | CTX_TApp
+  (* Existential Types *)
+  | CTX_Pack
+  | CTX_UnpackInL (e2 : expr)
+  | CTX_UnpackInR (e1 : expr)
   (* Concurrency *)
   | CTX_Fork
   (* Reference Types *)
@@ -43,11 +52,19 @@ Inductive ctx_item :=
   (* 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).
+  | CTX_CAS_R (e0 : expr) (e1 : expr)
+  (* Fetch and add for fine-grained concurrency *)
+  | CTX_FAA_L (e2 : expr)
+  | CTX_FAA_R (e1 : expr).
 
 Definition fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
   match ctx with
   | CTX_Rec => Rec e
+  | CTX_Lam => Lam e
+  | CTX_LetInL e2 => LetIn e e2
+  | CTX_LetInR e1 => LetIn e1 e
+  | CTX_SeqL e2 => Seq e e2
+  | CTX_SeqR e1 => Seq e1 e
   | CTX_AppL e2 => App e e2
   | CTX_AppR e1 => App e1 e
   | CTX_PairL e2 => Pair e e2
@@ -68,6 +85,9 @@ Definition fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
   | CTX_Unfold => Unfold e
   | CTX_TLam => TLam e
   | CTX_TApp => TApp e
+  | CTX_Pack => Pack e
+  | CTX_UnpackInL e2 => UnpackIn e e2
+  | CTX_UnpackInR e1 => UnpackIn e1 e
   | CTX_Fork => Fork e
   | CTX_Alloc => Alloc e
   | CTX_Load => Load e
@@ -76,6 +96,8 @@ Definition fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
   | 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
+  | CTX_FAA_L e2 => FAA e e2
+  | CTX_FAA_R e1 => FAA e1 e
   end.
 
 Definition ctx := list ctx_item.
@@ -87,6 +109,20 @@ Inductive typed_ctx_item :
     ctx_item → list type → type → list type → type → Prop :=
   | TP_CTX_Rec Γ τ τ' :
      typed_ctx_item CTX_Rec (TArrow τ τ' :: τ :: Γ) τ' Γ (TArrow τ τ')
+  | TP_CTX_Lam Γ τ τ' :
+     typed_ctx_item CTX_Lam (τ :: Γ) τ' Γ (TArrow τ τ')
+  | TP_CTX_LetInL Γ e2 τ τ' :
+     typed (τ :: Γ) e2 τ' →
+     typed_ctx_item (CTX_LetInL e2) Γ τ Γ τ'
+  | TP_CTX_LetInR Γ e1 τ τ' :
+     typed Γ e1 τ →
+     typed_ctx_item (CTX_LetInR e1) (τ :: Γ) τ' Γ τ'
+  | TP_CTX_SeqL Γ e2 τ τ' :
+     typed Γ e2 τ' →
+     typed_ctx_item (CTX_SeqL e2) Γ τ Γ τ'
+  | TP_CTX_SeqR Γ e1 τ τ' :
+     typed Γ e1 τ →
+     typed_ctx_item (CTX_SeqR e1) Γ τ' Γ τ'
   | TP_CTX_AppL Γ e2 τ τ' :
      typed Γ e2 τ →
      typed_ctx_item (CTX_AppL e2) Γ (TArrow τ τ') Γ τ'
@@ -125,12 +161,18 @@ Inductive typed_ctx_item :
   | TP_CTX_IfR Γ e0 e1 τ :
      typed Γ e0 (TBool) → typed Γ e1 τ →
      typed_ctx_item (CTX_IfR e0 e1) Γ τ Γ τ
-  | TP_CTX_BinOpL op Γ e2 :
-     typed Γ e2 TNat →
-     typed_ctx_item (CTX_BinOpL op e2) Γ TNat Γ (binop_res_type op)
-  | TP_CTX_BinOpR op e1 Γ :
-     typed Γ e1 TNat →
-     typed_ctx_item (CTX_BinOpR op e1) Γ TNat Γ (binop_res_type op)
+  | TP_CTX_int_BinOpL op Γ e2 :
+     typed Γ e2 TInt →
+     typed_ctx_item (CTX_BinOpL op e2) Γ TInt Γ (binop_res_type op)
+  | TP_CTX_int_BinOpR op e1 Γ :
+     typed Γ e1 TInt →
+     typed_ctx_item (CTX_BinOpR op e1) Γ TInt Γ (binop_res_type op)
+  | TP_CTX_Eq_BinOpL Γ e2 τ :
+     EqType τ → typed Γ e2 τ →
+     typed_ctx_item (CTX_BinOpL Eq e2) Γ τ Γ TBool
+  | TP_CTX_Eq_BinOpR e1 Γ τ :
+     EqType τ → typed Γ e1 τ →
+     typed_ctx_item (CTX_BinOpR Eq e1) Γ τ Γ TBool
   | TP_CTX_Fold Γ τ :
      typed_ctx_item CTX_Fold Γ τ.[(TRec τ)/] Γ (TRec τ)
   | TP_CTX_Unfold Γ τ :
@@ -139,6 +181,14 @@ Inductive typed_ctx_item :
      typed_ctx_item CTX_TLam (subst (ren (+1)) <$> Γ) τ Γ (TForall τ)
   | TP_CTX_TApp Γ τ τ' :
      typed_ctx_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/]
+  | TP_CTX_Pack Γ τ τ':
+     typed_ctx_item CTX_Pack Γ τ.[τ'/] Γ (TExist τ)
+  | TP_CTX_UnpackInL Γ e2 τ τ':
+     typed (τ :: (subst (ren (+1)) <$> Γ)) e2 τ'.[ren (+1)] →
+     typed_ctx_item (CTX_UnpackInL e2) Γ (TExist τ) Γ τ'
+  | TP_CTX_UnpackInR Γ e1 τ τ':
+     typed Γ e1 (TExist τ) →
+     typed_ctx_item (CTX_UnpackInR e1) (τ :: (subst (ren (+1)) <$> Γ)) τ'.[ren (+1)] Γ τ'
   | TP_CTX_Fork Γ :
      typed_ctx_item CTX_Fork Γ TUnit Γ TUnit
   | TPCTX_Alloc Γ τ :
@@ -158,7 +208,13 @@ Inductive typed_ctx_item :
      typed_ctx_item (CTX_CAS_M e0 e2) Γ τ Γ TBool
   | TP_CTX_CasR Γ e0 e1 τ :
      EqType τ → typed Γ e0 (Tref τ) → typed Γ e1 τ →
-     typed_ctx_item (CTX_CAS_R e0 e1) Γ τ Γ TBool.
+     typed_ctx_item (CTX_CAS_R e0 e1) Γ τ Γ TBool
+  | TP_CTX_FAA_L Γ e2 :
+     typed Γ e2 TInt →
+     typed_ctx_item (CTX_FAA_L e2) Γ (Tref TInt) Γ TInt
+  | TP_CTX_FAA_R Γ e1 :
+     typed Γ e1 (Tref TInt) →
+     typed_ctx_item (CTX_FAA_R e1) Γ TInt Γ TInt.
 
 Lemma typed_ctx_item_typed k Γ τ Γ' τ' e :
   typed Γ e τ → typed_ctx_item k Γ τ Γ' τ' →
@@ -187,7 +243,12 @@ Proof.
     repeat match goal with H : _ |- _ => rewrite fmap_length in H end;
     try f_equal;
     eauto using typed_n_closed;
-    try match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end.
+    try match goal with
+      | H : _ |- _ => by eapply (typed_n_closed _ _ _ H)
+      | H : _ |- _ => by let H' := fresh in
+                      pose proof (typed_n_closed _ _ _ H) as H';
+                      rewrite /= fmap_length in H'; eauto
+      end.
 Qed.
 
 Definition ctx_refines (Γ : list type)
@@ -249,6 +310,11 @@ Section bin_log_related_under_typed_ctx.
     iClear "H".
     inversion Hx1; subst; simpl; try fold_interp.
     - iApply bin_log_related_rec; done.
+    - iApply bin_log_related_lam; done.
+    - iApply bin_log_related_letin; last iApply binary_fundamental; done.
+    - iApply bin_log_related_letin; first iApply binary_fundamental; done.
+    - iApply bin_log_related_seq; last iApply binary_fundamental; done.
+    - iApply bin_log_related_seq; first iApply binary_fundamental; done.
     - iApply bin_log_related_app; last iApply binary_fundamental; done.
     - iApply bin_log_related_app; first iApply binary_fundamental; done.
     - iApply bin_log_related_pair; last iApply binary_fundamental; done.
@@ -269,12 +335,17 @@ Section bin_log_related_under_typed_ctx.
         [iApply binary_fundamental| |iApply binary_fundamental]; done.
     - iApply bin_log_related_if;
         [iApply binary_fundamental|iApply binary_fundamental|]; done.
-    - iApply bin_log_related_nat_binop; [|iApply binary_fundamental]; done.
-    - iApply bin_log_related_nat_binop; [iApply binary_fundamental|]; done.
+    - iApply bin_log_related_int_binop; [|iApply binary_fundamental]; done.
+    - iApply bin_log_related_int_binop; [iApply binary_fundamental|]; done.
+    - iApply bin_log_related_Eq_binop; [| |iApply binary_fundamental]; done.
+    - iApply bin_log_related_Eq_binop; [|iApply binary_fundamental|]; done.
     - iApply bin_log_related_fold; done.
     - iApply bin_log_related_unfold; done.
     - iApply bin_log_related_tlam; done.
     - iApply bin_log_related_tapp; done.
+    - iApply bin_log_related_pack; done.
+    - iApply bin_log_related_unpack; last iApply binary_fundamental; done.
+    - iApply bin_log_related_unpack; first iApply binary_fundamental; done.
     - iApply bin_log_related_fork; done.
     - iApply bin_log_related_alloc; done.
     - iApply bin_log_related_load; done.
@@ -286,5 +357,7 @@ Section bin_log_related_under_typed_ctx.
         [done|iApply binary_fundamental| |iApply binary_fundamental]; done.
     - iApply bin_log_related_CAS;
         [done|iApply binary_fundamental|iApply binary_fundamental|]; done.
+    - iApply bin_log_related_FAA; last iApply binary_fundamental; done.
+    - iApply bin_log_related_FAA; first iApply binary_fundamental; done.
   Qed.
 End bin_log_related_under_typed_ctx.
diff --git a/theories/logrel/F_mu_ref_conc/binary/examples/counter.v b/theories/logrel/F_mu_ref_conc/binary/examples/counter.v
index d9cbdef8fca70fd5ba7330448bfa01f1f7a29086..c4395502a4f06e6c4acab06452329d3c7d9f368f 100644
--- a/theories/logrel/F_mu_ref_conc/binary/examples/counter.v
+++ b/theories/logrel/F_mu_ref_conc/binary/examples/counter.v
@@ -41,7 +41,7 @@ Section CG_Counter.
 
   (* Coarse-grained increment *)
   Lemma CG_increment_type x Γ :
-    typed Γ x (Tref TNat) →
+    typed Γ x (Tref TInt) →
     typed Γ (CG_increment x) (TArrow TUnit TUnit).
   Proof.
     intros H1. repeat econstructor.
@@ -64,7 +64,7 @@ Section CG_Counter.
   Lemma steps_CG_increment E j K x n:
     nclose specN ⊆ E →
     spec_ctx ∗ x ↦ₛ (#nv n) ∗ j ⤇ fill K (App (CG_increment (Loc x)) Unit)
-      ⊢ |={E}=> j ⤇ fill K (Unit) ∗ x ↦ₛ (#nv (S n)).
+      ⊢ |={E}=> j ⤇ fill K (Unit) ∗ x ↦ₛ (#nv (1 + n)).
   Proof.
     iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_increment.
     iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
@@ -92,7 +92,7 @@ Section CG_Counter.
   Global Opaque CG_locked_incrementV.
 
   Lemma CG_locked_increment_type x l Γ :
-    typed Γ x (Tref TNat) →
+    typed Γ x (Tref TInt) →
     typed Γ l LockType →
     typed Γ (CG_locked_increment x l) (TArrow TUnit TUnit).
   Proof.
@@ -113,7 +113,7 @@ Section CG_Counter.
     nclose specN ⊆ E →
     spec_ctx ∗ x ↦ₛ (#nv n) ∗ l ↦ₛ (#♭v false)
       ∗ j ⤇ fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
-    ={E}=∗ j ⤇ fill K Unit ∗ x ↦ₛ (#nv S n) ∗ l ↦ₛ (#♭v false).
+    ={E}=∗ j ⤇ fill K Unit ∗ x ↦ₛ (#nv (1 + n)) ∗ l ↦ₛ (#♭v false).
   Proof.
     iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]".
     iMod (steps_with_lock
@@ -134,7 +134,7 @@ Section CG_Counter.
   Global Opaque counter_readV.
 
   Lemma counter_read_type x Γ :
-    typed Γ x (Tref TNat) → typed Γ (counter_read x) (TArrow TUnit TNat).
+    typed Γ x (Tref TInt) → typed Γ (counter_read x) (TArrow TUnit TInt).
   Proof.
     intros H1. repeat econstructor.
     eapply (context_weakening [_]); trivial.
@@ -168,10 +168,10 @@ Section CG_Counter.
   Local Opaque counter_read.
 
   Lemma CG_counter_body_type x l Γ :
-    typed Γ x (Tref TNat) →
+    typed Γ x (Tref TInt) →
     typed Γ l LockType →
     typed Γ (CG_counter_body x l)
-            (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
+            (TProd (TArrow TUnit TUnit) (TArrow TUnit TInt)).
   Proof.
     intros H1 H2; repeat econstructor;
       eauto using CG_locked_increment_type, counter_read_type.
@@ -184,7 +184,7 @@ Section CG_Counter.
   Hint Rewrite CG_counter_body_subst : autosubst.
 
   Lemma CG_counter_type Γ :
-    typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
+    typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TInt)).
   Proof.
     econstructor; eauto using newlock_type.
     econstructor; first eauto using typed.
@@ -198,7 +198,7 @@ Section CG_Counter.
 
   (* Fine-grained increment *)
   Lemma FG_increment_type x Γ :
-    typed Γ x (Tref TNat) →
+    typed Γ x (Tref TInt) →
     typed Γ (FG_increment x) (TArrow TUnit TUnit).
   Proof.
     intros Hx. do 3 econstructor; eauto using typed.
@@ -216,9 +216,9 @@ Section CG_Counter.
   Hint Rewrite FG_increment_subst : autosubst.
 
   Lemma FG_counter_body_type x Γ :
-    typed Γ x (Tref TNat) →
+    typed Γ x (Tref TInt) →
     typed Γ (FG_counter_body x)
-            (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
+            (TProd (TArrow TUnit TUnit) (TArrow TUnit TInt)).
   Proof.
     intros H1; econstructor.
     - apply FG_increment_type; trivial.
@@ -232,7 +232,7 @@ Section CG_Counter.
   Hint Rewrite FG_counter_body_subst : autosubst.
 
   Lemma FG_counter_type Γ :
-    Γ ⊢ₜ FG_counter : (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
+    Γ ⊢ₜ FG_counter : (TProd (TArrow TUnit TUnit) (TArrow TUnit TInt)).
   Proof.
     econstructor; eauto using newlock_type, typed.
     apply FG_counter_body_type; by constructor.
@@ -246,7 +246,7 @@ Section CG_Counter.
   Definition counterN : namespace := nroot .@ "counter".
 
   Lemma FG_CG_counter_refinement :
-    ⊢ [] ⊨ FG_counter ≤log≤ CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
+    ⊢ [] ⊨ FG_counter ≤log≤ CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TInt).
   Proof.
     iIntros (Δ [|??]) "!# #(Hspec & HΓ)"; iIntros (j K) "Hj"; last first.
     { iDestruct (interp_env_length with "HΓ") as %[=]. }
@@ -296,7 +296,7 @@ Section CG_Counter.
       { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". }
       iApply wp_pure_step_later; trivial. iAsimpl. iIntros "!> !> _".
       (* fine-grained performs increment *)
-      iApply (wp_bind (fill [CasRCtx (LocV _) (NatV _); IfCtx _ _]));
+      iApply (wp_bind (fill [CasRCtx (LocV _) (#nv _); IfCtx _ _]));
         iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
       iApply wp_pure_step_later; auto. iIntros "!> _". iApply wp_value.
       iApply (wp_bind (fill [IfCtx _ _]));
@@ -348,7 +348,7 @@ End CG_Counter.
 
 Theorem counter_ctx_refinement :
   [] ⊨ FG_counter ≤ctx≤ CG_counter :
-         TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
+         TProd (TArrow TUnit TUnit) (TArrow TUnit TInt).
 Proof.
   set (Σ := #[invΣ ; gen_heapΣ loc val ; soundness_binaryΣ ]).
   set (HG := soundness.HeapPreIG Σ _ _).
diff --git a/theories/logrel/F_mu_ref_conc/binary/examples/fact.v b/theories/logrel/F_mu_ref_conc/binary/examples/fact.v
index 599f9d3c92673d9267625deaa70e1e4b1271687f..dd010401fb8ac844970e4e2f4e2c3d3a1c24b73c 100644
--- a/theories/logrel/F_mu_ref_conc/binary/examples/fact.v
+++ b/theories/logrel/F_mu_ref_conc/binary/examples/fact.v
@@ -9,7 +9,7 @@ Definition fact : expr :=
           (#n 1)
           (BinOp Mult (Var 1) (App (Var 0) (BinOp Sub (Var 1) (#n 1))))).
 
-Lemma fact_typed : [] ⊢ₜ fact : TArrow TNat TNat.
+Lemma fact_typed : [] ⊢ₜ fact : TArrow TInt TInt.
 Proof. repeat econstructor. Qed.
 
 Definition fact_acc_body : expr :=
@@ -26,7 +26,7 @@ Definition fact_acc_body : expr :=
          )
       ).
 
-Lemma fact_acc_body_typed : [] ⊢ₜ fact_acc_body : TArrow TNat (TArrow TNat TNat).
+Lemma fact_acc_body_typed : [] ⊢ₜ fact_acc_body : TArrow TInt (TArrow TInt TInt).
 Proof. repeat econstructor. Qed.
 
 Lemma fact_acc_body_subst f : fact_acc_body.[f] = fact_acc_body.
@@ -56,7 +56,7 @@ Global Opaque fact_acc_body.
 Definition fact_acc : expr :=
   Lam (App (App fact_acc_body (Var 0)) (#n 1)).
 
-Lemma fact_acc_typed : [] ⊢ₜ fact_acc : TArrow TNat TNat.
+Lemma fact_acc_typed : [] ⊢ₜ fact_acc : TArrow TInt TInt.
 Proof.
   repeat econstructor.
   apply (closed_context_weakening [_] []); eauto.
@@ -67,7 +67,7 @@ Section fact_equiv.
   Context `{heapIG Σ, cfgSG Σ}.
 
   Lemma fact_fact_acc_refinement :
-    ⊢ [] ⊨ fact ≤log≤ fact_acc : (TArrow TNat TNat).
+    ⊢ [] ⊨ fact ≤log≤ fact_acc : (TArrow TInt TInt).
   Proof.
     iIntros (? vs) "!# [#HE HΔ]".
     iDestruct (interp_env_length with "HΔ") as %?; destruct vs; simplify_eq.
@@ -82,9 +82,11 @@ Section fact_equiv.
     asimpl.
     iApply (wp_mono _ _ _ (λ v, ∃ m, j ⤇ fill K (#n (1 * m)) ∗ ⌜v = #nv m⌝))%I.
     { iIntros (?). iDestruct 1 as (m) "[Hm %]"; subst.
+      replace (1 * m)%Z with m by lia.
       iExists (#nv _); iFrame; eauto. }
-    generalize 1 as l => l.
-    iInduction n as [|n] "IH" forall (l).
+    generalize 1%Z as l => l.
+    iLöb as "IH" forall (n l).
+    destruct (decide (n = 0)%Z) as [->|].
     - iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl; asimpl.
       rewrite fact_acc_body_unfold.
@@ -102,7 +104,7 @@ Section fact_equiv.
       iIntros "!> _"; simpl.
       iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
       iApply wp_value.
-      iExists 1. replace (l * 1) with l by lia.
+      iExists 1%Z. replace (l * 1)%Z with l by lia.
       auto.
     - iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl; asimpl.
@@ -115,10 +117,14 @@ Section fact_equiv.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl.
       iApply wp_value. simpl.
+      destruct (decide (n = 0)%Z); first lia.
+      rewrite bool_decide_eq_false_2; last done.
       iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
       simpl.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl.
+      destruct (decide (n = 0)%Z); first lia.
+      rewrite bool_decide_eq_false_2; last done.
       iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
       asimpl.
       iApply (wp_bind (fill [BinOpRCtx _ (#nv _)])).
@@ -133,19 +139,17 @@ Section fact_equiv.
       simpl.
       iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
       asimpl.
-      replace (n -0) with n by lia.
       iApply wp_wand_r; iSplitL; first iApply ("IH" with "[Hj]"); eauto.
       iIntros (v). iDestruct 1 as (m) "[H %]"; simplify_eq.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl; iApply wp_value.
-      iExists ((S n) * m); simpl.
-      replace (l * (m + n * m)) with ((l + n * l) * m)
-        by lia.
-      iFrame; auto.
+      iExists _; iSplit; last done.
+      replace (l * (n * m))%Z with (n * l * m)%Z by lia.
+      iFrame.
   Qed.
 
   Lemma fact_acc_fact_refinement :
-    ⊢ [] ⊨ fact_acc ≤log≤ fact : (TArrow TNat TNat).
+    ⊢ [] ⊨ fact_acc ≤log≤ fact : (TArrow TInt TInt).
   Proof.
     iIntros (? vs) "!# [#HE HΔ]".
     iDestruct (interp_env_length with "HΔ") as %?; destruct vs; simplify_eq.
@@ -160,10 +164,11 @@ Section fact_equiv.
     rewrite -/fact.
     iApply (wp_mono _ _ _ (λ v, ∃ m, j ⤇ fill K (#n m) ∗ ⌜v = #nv (1 * m)⌝))%I.
     { iIntros (?). iDestruct 1 as (m) "[? %]"; simplify_eq.
-      replace (1 * m) with m by lia.
+      replace (1 * m)%Z with m by lia.
       iExists (#nv _); iFrame; eauto. }
-    generalize 1 as l => l.
-    iInduction n as [|n] "IH" forall (K l).
+    generalize 1%Z as l => l.
+    iLöb as "IH" forall (K n l).
+    destruct (decide (n = 0)) as [->|].
     - rewrite fact_acc_body_unfold.
       iApply (wp_bind (fill [AppLCtx _])).
       iApply wp_pure_step_later; auto.
@@ -183,8 +188,7 @@ Section fact_equiv.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl.
       iApply wp_value.
-      iExists 1.
-      replace (l * 1) with l by lia; auto.
+      iExists 1%Z. replace (l * 1)%Z with l by lia; auto.
     - rewrite {2}fact_acc_body_unfold.
       iApply (wp_bind (fill [AppLCtx _])).
       iApply wp_pure_step_later; auto.
@@ -199,10 +203,14 @@ Section fact_equiv.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl.
       iApply wp_value. simpl.
+      destruct (decide (n = 0)%Z); first lia.
+      rewrite bool_decide_eq_false_2; last done.
       iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
       simpl.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl.
+      destruct (decide (n = 0)%Z); first lia.
+      rewrite bool_decide_eq_false_2; last done.
       iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
       iMod (do_step_pure _ _ (AppRCtx (RecV _):: BinOpRCtx _ (#nv _) :: _)
               with "[$Hj]") as "Hj"; eauto.
@@ -217,7 +225,6 @@ Section fact_equiv.
       iIntros "!> _"; simpl; iApply wp_value; simpl.
       iApply wp_pure_step_later; auto.
       iIntros "!> _"; simpl. asimpl.
-      replace (n -0) with n by lia.
       iApply wp_fupd.
       iApply wp_wand_r; iSplitL;
         first iApply ("IH" $! (BinOpRCtx _ (#nv _) :: K) with "[$Hj]"); eauto.
@@ -226,16 +233,16 @@ Section fact_equiv.
       iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
       simpl.
       iModIntro.
-      iExists (S n * m).
-      iFrame.
-      eauto with lia.
+      iExists _; iSplit; first by iFrame.
+      replace (l * (n * m))%Z with (n * l * m)%Z by lia.
+      done.
   Qed.
 
 End fact_equiv.
 
 Theorem fact_ctx_equiv :
-  [] ⊨ fact ≤ctx≤ fact_acc : (TArrow TNat TNat) ∧
-  [] ⊨ fact_acc ≤ctx≤ fact : (TArrow TNat TNat).
+  [] ⊨ fact ≤ctx≤ fact_acc : (TArrow TInt TInt) ∧
+  [] ⊨ fact_acc ≤ctx≤ fact : (TArrow TInt TInt).
 Proof.
   set (Σ := #[invΣ ; gen_heapΣ loc val ; soundness_binaryΣ]).
   set (HG := soundness.HeapPreIG Σ _ _).
diff --git a/theories/logrel/F_mu_ref_conc/binary/fundamental.v b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
index 83d8c417ee3155426c093959b8f6d68cb8a8d65c..497cf8856df3bdbb3526800611ca495601a406a1 100644
--- a/theories/logrel/F_mu_ref_conc/binary/fundamental.v
+++ b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
@@ -77,7 +77,7 @@ Section fundamental.
     iApply wp_value. iExists UnitV; eauto.
   Qed.
 
-  Lemma bin_log_related_nat Γ n : ⊢ Γ ⊨ #n n ≤log≤ #n n : TNat.
+  Lemma bin_log_related_int Γ n : ⊢ Γ ⊨ #n n ≤log≤ #n n : TInt.
   Proof.
     iIntros (Δ vvs) "!# #(Hs & HΓ)"; iIntros (j K) "Hj /=".
     iApply wp_value. iExists (#nv _); eauto.
@@ -197,9 +197,9 @@ Section fundamental.
       iApply (bin_log_related_alt with "IH3"); eauto.
   Qed.
 
-  Lemma bin_log_related_nat_binop Γ op e1 e2 e1' e2' :
-    Γ ⊨ e1 ≤log≤ e1' : TNat -∗
-    Γ ⊨ e2 ≤log≤ e2' : TNat -∗
+  Lemma bin_log_related_int_binop Γ op e1 e2 e1' e2' :
+    Γ ⊨ e1 ≤log≤ e1' : TInt -∗
+    Γ ⊨ e2 ≤log≤ e2' : TInt -∗
     Γ ⊨ BinOp op e1 e2 ≤log≤ BinOp op e1' e2' : binop_res_type op.
   Proof.
     iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)".
@@ -211,11 +211,34 @@ Section fundamental.
     iDestruct "Hvv" as (n) "[% %]"; simplify_eq/=.
     iDestruct "Hww" as (n') "[% %]"; simplify_eq/=.
     iApply fupd_wp.
-    iMod (step_nat_binop _ j K with "[-]") as "Hz"; eauto.
+    iMod (step_int_binop _ j K with "[-]") as "Hz"; eauto.
     iApply wp_pure_step_later; auto. iIntros "!> !> _".
     iApply wp_value. iExists _; iSplitL; eauto.
-    destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
-      try destruct lt_dec; eauto.
+    destruct op; simpl; try destruct Z.eq_dec; try destruct Z.le_dec;
+      try destruct Z.lt_dec; eauto.
+  Qed.
+
+  Lemma bin_log_related_Eq_binop Γ e1 e2 e1' e2' τ :
+    EqType τ →
+    Γ ⊨ e1 ≤log≤ e1' : τ -∗
+    Γ ⊨ e2 ≤log≤ e2' : τ -∗
+    Γ ⊨ BinOp Eq e1 e2 ≤log≤ BinOp Eq e1' e2' : TBool.
+  Proof.
+    intros HEQT.
+    iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)".
+    iApply (interp_expr_bind' [BinOpLCtx _ _] [BinOpLCtx _ _]); first by iApply "IH1"; iFrame "#".
+    iIntros ([v v']) "#Hvv".
+    iApply (interp_expr_bind' [BinOpRCtx _ _] [BinOpRCtx _ _]); first by iApply "IH2"; iFrame "#".
+    iIntros ([w w']) "#Hww /=".
+    iIntros (j K) "Hj /=".
+    iMod (EqType_interp_one_to_one with "Hvv Hww") as "%Hvals"; first done.
+    iMod (step_Eq_binop _ j K with "[-]") as "Hz"; eauto; try apply _.
+    iApply wp_pure_step_later; auto. iIntros "!> _".
+    iApply wp_value. iExists _; iSplitL; eauto.
+    destruct (decide (v = w)) as [Hvw|Hvw];
+      pose proof Hvw as Hvw'; rewrite Hvals in Hvw'.
+    - rewrite !bool_decide_eq_true_2; auto with f_equal.
+    - rewrite !bool_decide_eq_false_2; try intros ?%of_val_inj; done.
   Qed.
 
   Lemma bin_log_related_rec Γ e e' τ1 τ2 :
@@ -490,7 +513,8 @@ Section fundamental.
     destruct (decide (v = w)) as [|Hneq]; simplify_eq.
     - iApply (wp_cas_suc with "Hl"); eauto using to_of_val; eauto.
       iNext. iIntros "Hl".
-      iMod (interp_EqType_one_to_one with "Hl Hl' Hvv Hww") as "(Hl & Hl' & %)"; first done.
+      iMod (EqType_interp_CAS with "Hl Hl' Hvv Hww") as "(Hl & Hl' & %Hvw)";
+        first done.
       destruct (decide (v' = w')); simplify_eq; last by intuition simplify_eq.
       iMod (step_cas_suc with "[$]") as "[Hw Hl']"; simpl; eauto; first solve_ndisj.
       iMod ("Hclose" with "[Hl Hl']").
@@ -498,7 +522,8 @@ Section fundamental.
       iExists (#â™­v true); iFrame; eauto.
     - iApply (wp_cas_fail with "Hl"); eauto using to_of_val; eauto.
       iNext. iIntros "Hl".
-      iMod (interp_EqType_one_to_one with "Hl Hl' Hvv Hww") as "(Hl & Hl' & %)"; first done.
+      iMod (EqType_interp_CAS with "Hl Hl' Hvv Hww") as "(Hl & Hl' & %)";
+        first done.
       destruct (decide (v' = w')); simplify_eq; first by intuition simplify_eq.
       iMod (step_cas_fail with "[$]") as "[Hw Hl']"; simpl; eauto; first solve_ndisj.
       iMod ("Hclose" with "[Hl Hl']").
@@ -507,9 +532,9 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_FAA Γ e1 e2 e1' e2' :
-    Γ ⊨ e1 ≤log≤ e1' : Tref TNat -∗
-    Γ ⊨ e2 ≤log≤ e2' : TNat -∗
-    Γ ⊨ FAA e1 e2 ≤log≤ FAA e1' e2' : TNat.
+    Γ ⊨ e1 ≤log≤ e1' : Tref TInt -∗
+    Γ ⊨ e2 ≤log≤ e2' : TInt -∗
+    Γ ⊨ FAA e1 e2 ≤log≤ FAA e1' e2' : TInt.
   Proof.
     iIntros "#IH1 #IH2" (Δ vvs) "!# #(Hs & HΓ)".
     iApply (interp_expr_bind' [FAALCtx _] [FAALCtx _]); first by iApply "IH1"; iFrame "#".
@@ -538,9 +563,10 @@ Section fundamental.
     induction 1.
     - iApply bin_log_related_var; done.
     - iApply bin_log_related_unit.
-    - iApply bin_log_related_nat.
+    - iApply bin_log_related_int.
     - iApply bin_log_related_bool.
-    - iApply bin_log_related_nat_binop; done.
+    - iApply bin_log_related_int_binop; done.
+    - iApply bin_log_related_Eq_binop; done.
     - iApply bin_log_related_pair; done.
     - iApply bin_log_related_fst; done.
     - iApply bin_log_related_snd; done.
diff --git a/theories/logrel/F_mu_ref_conc/binary/logrel.v b/theories/logrel/F_mu_ref_conc/binary/logrel.v
index 3b25de1d7bbb41933c5a814a80e88ecb425e83ff..b17a873f5cf80853cf90f907f142e61793ebc101 100644
--- a/theories/logrel/F_mu_ref_conc/binary/logrel.v
+++ b/theories/logrel/F_mu_ref_conc/binary/logrel.v
@@ -39,8 +39,8 @@ Section logrel.
 
   Program Definition interp_unit : listO D -n> D :=
     λne Δ, PersPred (λ ww, ⌜ww.1 = UnitV⌝ ∧ ⌜ww.2 = UnitV⌝)%I.
-  Program Definition interp_nat : listO D -n> D :=
-    λne Δ, PersPred (λ ww, ∃ n : nat, ⌜ww.1 = #nv n⌝ ∧ ⌜ww.2 = #nv n⌝)%I.
+  Program Definition interp_int : listO D -n> D :=
+    λne Δ, PersPred (λ ww, ∃ n : Z, ⌜ww.1 = #nv n⌝ ∧ ⌜ww.2 = #nv n⌝)%I.
 
   Program Definition interp_bool : listO D -n> D :=
     λne Δ, PersPred (λ ww, ∃ b : bool, ⌜ww.1 = #♭v b⌝ ∧ ⌜ww.2 = #♭v b⌝)%I.
@@ -125,7 +125,7 @@ Section logrel.
   Fixpoint interp (Ï„ : type) : listO D -n> D :=
     match Ï„ return _ with
     | TUnit => interp_unit
-    | TNat => interp_nat
+    | TInt => interp_int
     | TBool => interp_bool
     | TProd Ï„1 Ï„2 => interp_prod (interp Ï„1) (interp Ï„2)
     | TSum Ï„1 Ï„2 => interp_sum (interp Ï„1) (interp Ï„2)
@@ -230,7 +230,38 @@ Section logrel.
     apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
   Qed.
 
-  Lemma interp_EqType_one_to_one Δ τ l l' u u' v v' w w' :
+  Lemma EqType_interp_one_to_one Δ τ v v' w w' :
+    EqType τ →
+    ⟦ τ ⟧ Δ (v, v') -∗
+    ⟦ τ ⟧ Δ (w, w') ={⊤}=∗
+    ⌜v = w ↔ v' = w'⌝.
+  Proof.
+    iIntros (Heqt) "Hvv Hww".
+    destruct Ï„; inversion Heqt; simplify_eq/=.
+    { iDestruct "Hvv"as "[% %]"; simplify_eq.
+      iDestruct "Hww"as "[% %]"; simplify_eq.
+      by iFrame. }
+    { iDestruct "Hvv"as "(%&%&%)"; simplify_eq.
+      iDestruct "Hww"as "(%&%&%)"; simplify_eq.
+      by iFrame. }
+    { iDestruct "Hvv"as "(%&%&%)"; simplify_eq.
+      iDestruct "Hww"as "(%&%&%)"; simplify_eq.
+      by iFrame. }
+    iDestruct "Hvv" as ([l1 l1']) "[% Hll1]"; simplify_eq/=.
+    iDestruct "Hww" as ([l2 l2']) "[% Hll2]"; simplify_eq/=.
+    destruct (decide (l1 = l2)) as [->|].
+    - destruct (decide (l1' = l2')) as [->|]; first done.
+      + iInv (logN.@(l2, l1')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
+        iInv (logN.@(l2, l2')) as ([w w']) "(>Hly & >Hly' & Hww) /=" "Hclose'".
+        iCombine "Hlx Hly" gives %[? ?]; done.
+    - destruct (decide (l1' = l2')) as [->|]; last first.
+      { iPureIntro; intuition; simplify_eq. }
+      iInv (logN.@(l1, l2')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
+      iInv (logN.@(l2, l2')) as ([w w']) "(>Hly & >Hly' & Hww) /=" "Hclose'".
+      iCombine "Hlx' Hly'" gives %[? ?]; done.
+  Qed.
+
+  Lemma EqType_interp_CAS Δ τ l l' u u' v v' w w' :
     EqType τ →
     l ↦ᵢ u -∗
     l' ↦ₛ u' -∗
diff --git a/theories/logrel/F_mu_ref_conc/binary/rules.v b/theories/logrel/F_mu_ref_conc/binary/rules.v
index 49df469069d10bef82228e75bff7e256254d95d9..6393e76ff80ecdcb953971094bb5b79d57b8ee7c 100644
--- a/theories/logrel/F_mu_ref_conc/binary/rules.v
+++ b/theories/logrel/F_mu_ref_conc/binary/rules.v
@@ -495,10 +495,18 @@ Section cfg.
     spec_ctx ∗ j ⤇ fill K (If (#♭ true) e1 e2) ={E}=∗ j ⤇ fill K e1.
   Proof. by intros; apply: do_step_pure. Qed.
 
-  Lemma step_nat_binop E j K op a b :
+  Lemma step_int_binop E j K op a b :
     nclose specN ⊆ E →
     spec_ctx ∗ j ⤇ fill K (BinOp op (#n a) (#n b))
-      ={E}=∗ j ⤇ fill K (of_val (binop_eval op a b)).
+      ={E}=∗ j ⤇ fill K (of_val (int_binop_eval op a b)).
+  Proof. by intros; apply: do_step_pure. Qed.
+
+  Lemma step_Eq_binop E j K e1 e2 v1 v2 :
+    to_val e1 = Some v1 →
+    to_val e2 = Some v2 →
+    nclose specN ⊆ E →
+    spec_ctx ∗ j ⤇ fill K (BinOp Eq e1 e2)
+      ={E}=∗ j ⤇ fill K (#♭ (bool_decide (e1 = e2))).
   Proof. by intros; apply: do_step_pure. Qed.
 
   Lemma step_fork E j K e :
diff --git a/theories/logrel/F_mu_ref_conc/lang.v b/theories/logrel/F_mu_ref_conc/lang.v
index 44012e02ba40c16d7518035311c3ae0555a42748..2c8303f1f88d85826f846cdebc16b093902b93dd 100644
--- a/theories/logrel/F_mu_ref_conc/lang.v
+++ b/theories/logrel/F_mu_ref_conc/lang.v
@@ -23,7 +23,7 @@ Module F_mu_ref_conc.
   | Seq (e1 e2 : expr)
   (* Base Types *)
   | Unit
-  | Nat (n : nat)
+  | Int (n : Z)
   | Bool (b : bool)
   | BinOp (op : binop) (e1 e2 : expr)
   (* If then else *)
@@ -63,7 +63,7 @@ Module F_mu_ref_conc.
 
   (* Notation for bool and nat *)
   Notation "#â™­ b" := (Bool b) (at level 20).
-  Notation "#n n" := (Nat n) (at level 20).
+  Notation "#n n" := (Int n) (at level 20).
 
   Global Instance expr_dec_eq (e e' : expr) : Decision (e = e').
   Proof. solve_decision. Defined.
@@ -74,7 +74,7 @@ Module F_mu_ref_conc.
   | TLamV (e : {bind 1 of expr})
   | PackV (v : val)
   | UnitV
-  | NatV (n : nat)
+  | IntV (n : Z)
   | BoolV (b : bool)
   | PairV (v1 v2 : val)
   | InjLV (v : val)
@@ -84,20 +84,30 @@ Module F_mu_ref_conc.
 
   (* Notation for bool and nat *)
   Notation "'#â™­v' b" := (BoolV b) (at level 20).
-  Notation "'#nv' n" := (NatV n) (at level 20).
+  Notation "'#nv' n" := (IntV n) (at level 20).
 
-  Definition binop_eval (op : binop) : nat → nat → val :=
+  Global Instance val_dec_eq (v v' : val) : Decision (v = v').
+  Proof. solve_decision. Defined.
+
+  Definition int_binop_eval (op : binop) : Z → Z → val :=
     match op with
     | Add => λ a b, #nv(a + b)
     | Sub => λ a b, #nv(a - b)
     | Mult => λ a b, #nv(a * b)
-    | Eq => λ a b, if (eq_nat_dec a b) then #♭v true else #♭v false
-    | Le => λ a b, if (le_dec a b) then #♭v true else #♭v false
-    | Lt => λ a b, if (lt_dec a b) then #♭v true else #♭v false
+    | Eq => λ a b, #♭v (bool_decide (a = b))
+    | Le => λ a b, #♭v (bool_decide (a ≤ b)%Z)
+    | Lt => λ a b, #♭v (bool_decide (a < b)%Z)
     end.
 
-  Global Instance val_dec_eq (v v' : val) : Decision (v = v').
-  Proof. solve_decision. Defined.
+  Definition binop_eval (op : binop) : val → val → option val :=
+    match op with
+    | Eq => λ a b, Some (#♭v (bool_decide (a = b)))
+    | _ => λ a b,
+        match a, b with
+        | IntV an, IntV bn => Some (int_binop_eval op an bn)
+        | _, _ => None
+        end
+    end.
 
   Global Instance val_inh : Inhabited val := populate UnitV.
 
@@ -108,7 +118,7 @@ Module F_mu_ref_conc.
     | TLamV e => TLam e
     | PackV v => Pack (of_val v)
     | UnitV => Unit
-    | NatV v => Nat v
+    | IntV v => Int v
     | BoolV v => Bool v
     | PairV v1 v2 => Pair (of_val v1) (of_val v2)
     | InjLV v => InjL (of_val v)
@@ -124,7 +134,7 @@ Module F_mu_ref_conc.
     | TLam e => Some (TLamV e)
     | Pack e => PackV <$> to_val e
     | Unit => Some UnitV
-    | Nat n => Some (NatV n)
+    | Int n => Some (IntV n)
     | Bool b => Some (BoolV b)
     | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
     | InjL e => InjLV <$> to_val e
@@ -231,8 +241,11 @@ Module F_mu_ref_conc.
       to_val e0 = Some v0 →
       base_step (Case (InjR e0) e1 e2) σ [] e2.[e0/] σ []
     (* nat bin op *)
-  | BinOpS op a b σ :
-      base_step (BinOp op (#n a) (#n b)) σ [] (of_val (binop_eval op a b)) σ []
+  | BinOpS op a av b bv rv σ :
+      to_val a = Some av →
+      to_val b = Some bv →
+      binop_eval op av bv = Some rv →
+      base_step (BinOp op a b) σ [] (of_val rv) σ []
   (* If then else *)
   | IfFalse e1 e2 σ :
       base_step (If (#♭ false) e1 e2) σ [] e2 σ []
@@ -272,9 +285,9 @@ Module F_mu_ref_conc.
      σ !! l = Some v1 →
      base_step (CAS (Loc l) e1 e2) σ [] (#♭ true) (<[l:=v2]>σ) []
   | FAAS l m e2 k σ :
-      to_val e2 = Some (NatV k) →
-      σ !! l = Some (NatV m) →
-      base_step (FAA (Loc l) e2) σ [] (#n m) (<[l:=NatV (m + k)]>σ) [].
+      to_val e2 = Some (IntV k) →
+      σ !! l = Some (IntV m) →
+      base_step (FAA (Loc l) e2) σ [] (#n m) (<[l:=IntV (m + k)]>σ) [].
 
   (** Basic properties about the language *)
   Lemma to_of_val v : to_val (of_val v) = Some v.
diff --git a/theories/logrel/F_mu_ref_conc/typing.v b/theories/logrel/F_mu_ref_conc/typing.v
index 29eff71cd36bdd4f034aa0dcd2225520c76c3a5e..c6af41f769c82189425b319367d62abf9334b55c 100644
--- a/theories/logrel/F_mu_ref_conc/typing.v
+++ b/theories/logrel/F_mu_ref_conc/typing.v
@@ -3,7 +3,7 @@ From iris.prelude Require Import options.
 
 Inductive type :=
   | TUnit : type
-  | TNat : type
+  | TInt : type
   | TBool : type
   | TProd : type → type → type
   | TSum : type → type → type
@@ -21,13 +21,13 @@ Global Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
 
 Definition binop_res_type (op : binop) : type :=
   match op with
-  | Add => TNat | Sub => TNat | Mult => TNat
+  | Add => TInt | Sub => TInt | Mult => TInt
   | Eq => TBool | Le => TBool | Lt => TBool
   end.
 
 Inductive EqType : type → Prop :=
   | EqTUnit : EqType TUnit
-  | EqTNat : EqType TNat
+  | EqTNat : EqType TInt
   | EqTBool : EqType TBool
   | EQRef Ï„ : EqType (Tref Ï„).
 
@@ -36,11 +36,21 @@ Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
 Inductive typed (Γ : list type) : expr → type → Prop :=
   | Var_typed x τ : Γ !! x = Some τ → Γ ⊢ₜ Var x : τ
   | Unit_typed : Γ ⊢ₜ Unit : TUnit
-  | Nat_typed n : Γ ⊢ₜ #n n : TNat
+  | Int_typed n : Γ ⊢ₜ #n n : TInt
   | Bool_typed b : Γ ⊢ₜ #♭ b : TBool
-  | BinOp_typed op e1 e2 :
-     Γ ⊢ₜ e1 : TNat → Γ ⊢ₜ e2 : TNat → Γ ⊢ₜ BinOp op e1 e2 : binop_res_type op
-  | Pair_typed e1 e2 τ1 τ2 : Γ ⊢ₜ e1 : τ1 → Γ ⊢ₜ e2 : τ2 → Γ ⊢ₜ Pair e1 e2 : TProd τ1 τ2
+  | Int_BinOp_typed op e1 e2 :
+     Γ ⊢ₜ e1 : TInt →
+     Γ ⊢ₜ e2 : TInt →
+     Γ ⊢ₜ BinOp op e1 e2 : binop_res_type op
+  | Eq_typed e1 e2 Ï„ :
+     EqType τ →
+     Γ ⊢ₜ e1 : τ →
+     Γ ⊢ₜ e2 : τ →
+     Γ ⊢ₜ BinOp Eq e1 e2 : TBool
+  | Pair_typed e1 e2 Ï„1 Ï„2 :
+     Γ ⊢ₜ e1 : τ1 →
+     Γ ⊢ₜ e2 : τ2 →
+     Γ ⊢ₜ Pair e1 e2 : TProd τ1 τ2
   | Fst_typed e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Fst e : τ1
   | Snd_typed e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Snd e : τ2
   | InjL_typed e τ1 τ2 : Γ ⊢ₜ e : τ1 → Γ ⊢ₜ InjL e : TSum τ1 τ2
@@ -78,7 +88,7 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
   | TCAS e1 e2 e3 Ï„ :
      EqType τ → Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
      Γ ⊢ₜ CAS e1 e2 e3 : TBool
-  | TFAA e1 e2 : Γ ⊢ₜ e1 : Tref TNat → Γ ⊢ₜ e2 : TNat → Γ ⊢ₜ FAA e1 e2 : TNat
+  | TFAA e1 e2 : Γ ⊢ₜ e1 : Tref TInt → Γ ⊢ₜ e2 : TInt → Γ ⊢ₜ FAA e1 e2 : TInt
 where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
 
 Fixpoint env_subst (vs : list val) : var → expr :=
diff --git a/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v b/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
index 11439b0f73a0d5b999e8a30821f71eb63858dc97..f33cd53b5af8f0a3d9dfcc22fe3ec17fda347abc 100644
--- a/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
+++ b/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
@@ -66,11 +66,11 @@ Section symbol_nat_sem_typ.
     iNext. iIntros (l) "Hl".
     iApply wp_pure_step_later; auto. iIntros "!> _". asimpl.
     iMod Token_init as (γ) "Hmt".
-    iMod (inv_alloc (nroot .@ "tk") _ (∃ t, l ↦ᵢ (#nv t) ∗ Max_token γ t)
+    iMod (inv_alloc (nroot .@ "tk") _ (∃ t : nat, l ↦ᵢ (#nv t) ∗ Max_token γ t)
             with "[Hl Hmt]") as "#Hinv".
     { unfold Max_token. by iNext; iExists _; iFrame. }
     iApply wp_value.
-    iExists (PersPred (λ v, ∃ m, ⌜v = #nv m⌝ ∗ Token γ m))%I; simpl.
+    iExists (PersPred (λ v, ∃ m : nat, ⌜v = #nv m⌝ ∗ Token γ m))%I; simpl.
     iExists _; iSplit; first done.
     iExists _, _; iSplit; first done.
     iSplit.
@@ -84,6 +84,7 @@ Section symbol_nat_sem_typ.
       iNext. iIntros "Hl".
       iMod (Token_alloc with "Hmt") as "[Hmt Htk]".
       iMod ("Hcl" with "[Hl Hmt]") as "_"; last by eauto.
+      replace (t + 1)%Z with ((t + 1)%nat : Z) by lia.
       iNext; iExists _; iFrame.
     - iModIntro.
       iIntros (w). iDestruct 1 as (m ?) "Htk"; simplify_eq.
@@ -101,7 +102,9 @@ Section symbol_nat_sem_typ.
       iModIntro.
       simpl.
       iApply wp_pure_step_later; auto. iIntros "!> _".
-      simpl. destruct lt_dec; last done. simpl.
+      simpl.
+      destruct (decide (m < t)%Z); last lia.
+      rewrite bool_decide_eq_true_2; last done.
       iApply wp_value.
       iApply wp_pure_step_later; auto. iIntros "!> _".
       iApply wp_value; eauto.
diff --git a/theories/logrel/F_mu_ref_conc/unary/fundamental.v b/theories/logrel/F_mu_ref_conc/unary/fundamental.v
index 559a3a2f471823e4f01db272f057d1aa5d688977..0af0f81b07db06645d931ad086948bb88cb0bbfc 100644
--- a/theories/logrel/F_mu_ref_conc/unary/fundamental.v
+++ b/theories/logrel/F_mu_ref_conc/unary/fundamental.v
@@ -29,14 +29,14 @@ Section typed_interp.
   Lemma sem_typed_unit Γ : ⊢ Γ ⊨ Unit : TUnit.
   Proof. iIntros (Δ vs) "!# #HΓ". iApply wp_value; done. Qed.
 
-  Lemma sem_typed_nat Γ n : ⊢ Γ ⊨ #n n : TNat.
+  Lemma sem_typed_int Γ n : ⊢ Γ ⊨ #n n : TInt.
   Proof. iIntros (Δ vs) "!# #HΓ /=". iApply wp_value; eauto. Qed.
 
   Lemma sem_typed_bool Γ b : ⊢ Γ ⊨ #♭ b : TBool.
   Proof. iIntros (Δ vs) "!# #HΓ /=". iApply wp_value; eauto. Qed.
 
-  Lemma sem_typed_nat_binop Γ op e1 e2 :
-    Γ ⊨ e1 : TNat -∗ Γ ⊨ e2 : TNat -∗ Γ ⊨ BinOp op e1 e2 : binop_res_type op.
+  Lemma sem_typed_int_binop Γ op e1 e2 :
+    Γ ⊨ e1 : TInt -∗ Γ ⊨ e2 : TInt -∗ Γ ⊨ BinOp op e1 e2 : binop_res_type op.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ /=".
     iApply (interp_expr_bind [BinOpLCtx _ _]); first by iApply "IH1".
@@ -45,11 +45,25 @@ Section typed_interp.
     iIntros (w) "#Hw/=".
     iDestruct "Hv" as (n) "%"; iDestruct "Hw" as (n') "%"; simplify_eq/=.
     iApply wp_pure_step_later; [done|]; iIntros "!> _". iApply wp_value.
-    destruct op; simpl; try destruct eq_nat_dec;
-      try destruct le_dec; try destruct lt_dec; eauto 10.
+    destruct op; simpl; try destruct Z.eq_dec;
+      try destruct Z.le_dec; try destruct Z.lt_dec; eauto 10.
   Qed.
 
-  Lemma sem_typed_pair Γ e1 e2 τ1 τ2 : Γ ⊨ e1 : τ1 -∗ Γ ⊨ e2 : τ2 -∗ Γ ⊨ Pair e1 e2 : TProd τ1 τ2.
+  Lemma sem_typed_Eq_binop Γ e1 e2 τ :
+    Γ ⊨ e1 : τ -∗ Γ ⊨ e2 : τ -∗ Γ ⊨ BinOp Eq e1 e2 : TBool.
+  Proof.
+    iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ /=".
+    iApply (interp_expr_bind [BinOpLCtx _ _]); first by iApply "IH1".
+    iIntros (v) "#Hv /=".
+    iApply (interp_expr_bind [BinOpRCtx _ _]); first by iApply "IH2".
+    iIntros (w) "#Hw/=".
+    iApply wp_pure_step_later; [done|]; iIntros "!> _". iApply wp_value; eauto.
+  Qed.
+
+  Lemma sem_typed_pair Γ e1 e2 τ1 τ2 :
+    Γ ⊨ e1 : τ1 -∗
+    Γ ⊨ e2 : τ2 -∗
+    Γ ⊨ Pair e1 e2 : TProd τ1 τ2.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ"; simpl.
     iApply (interp_expr_bind [PairLCtx _]); first by iApply "IH1".
@@ -317,7 +331,10 @@ Section typed_interp.
       iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
   Qed.
 
-  Lemma sem_typed_FAA Γ e1 e2 : Γ ⊨ e1 : Tref TNat -∗ Γ ⊨ e2 : TNat -∗ Γ ⊨ FAA e1 e2 : TNat.
+  Lemma sem_typed_FAA Γ e1 e2 :
+    Γ ⊨ e1 : Tref TInt -∗
+    Γ ⊨ e2 : TInt -∗
+    Γ ⊨ FAA e1 e2 : TInt.
   Proof.
     iIntros "#IH1 #IH2" (Δ vs) "!# #HΓ /=".
     iApply (interp_expr_bind [FAALCtx _]); first by iApply "IH1".
@@ -341,9 +358,10 @@ Section typed_interp.
     induction 1.
     - iApply sem_typed_var; done.
     - iApply sem_typed_unit; done.
-    - iApply sem_typed_nat; done.
+    - iApply sem_typed_int; done.
     - iApply sem_typed_bool; done.
-    - iApply sem_typed_nat_binop; done.
+    - iApply sem_typed_int_binop; done.
+    - iApply sem_typed_Eq_binop; done.
     - iApply sem_typed_pair; done.
     - iApply sem_typed_fst; done.
     - iApply sem_typed_snd; done.
diff --git a/theories/logrel/F_mu_ref_conc/unary/logrel.v b/theories/logrel/F_mu_ref_conc/unary/logrel.v
index ac3b6fa2cc7051735ccff67b242a16566b94d3df..95ab074fdf31ed4925d2345e6f4ee33bd1838f6e 100644
--- a/theories/logrel/F_mu_ref_conc/unary/logrel.v
+++ b/theories/logrel/F_mu_ref_conc/unary/logrel.v
@@ -24,7 +24,7 @@ Section logrel.
   Solve Obligations with repeat intros ?; simpl; solve_proper.
 
   Definition interp_unit : listO D -n> D := λne Δ, PersPred (λ w, ⌜w = UnitV⌝)%I.
-  Definition interp_nat : listO D -n> D :=
+  Definition interp_int : listO D -n> D :=
     λne Δ, PersPred (λ w, ⌜∃ n, w = #nv n⌝)%I.
   Definition interp_bool : listO D -n> D :=
     λne Δ, PersPred (λ w, ⌜∃ n, w = #♭v n⌝)%I.
@@ -90,7 +90,7 @@ Section logrel.
   Fixpoint interp (Ï„ : type) : listO D -n> D :=
     match Ï„ return _ with
     | TUnit => interp_unit
-    | TNat => interp_nat
+    | TInt => interp_int
     | TBool => interp_bool
     | TProd Ï„1 Ï„2 => interp_prod (interp Ï„1) (interp Ï„2)
     | TSum Ï„1 Ï„2 => interp_sum (interp Ï„1) (interp Ï„2)
diff --git a/theories/logrel/F_mu_ref_conc/wp_rules.v b/theories/logrel/F_mu_ref_conc/wp_rules.v
index b0d7b9e0cdc98a79a088f8dc9502a5efb9a19788..08f811f2122c9b496f3055f26797afea5e9cf4fc 100644
--- a/theories/logrel/F_mu_ref_conc/wp_rules.v
+++ b/theories/logrel/F_mu_ref_conc/wp_rules.v
@@ -140,8 +140,17 @@ Section lang_rules.
     iNext; iIntros (v2 σ2 efs Hstep) "_"; inv_base_step. by iFrame.
   Qed.
 
-  Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
-  Local Ltac solve_exec_puredet := simpl; intros; by inv_base_step.
+  Local Ltac solve_exec_safe :=
+    intros; subst; do 3 eexists; econstructor; simpl; eauto.
+  Local Ltac solve_exec_puredet :=
+    simpl; intros;
+      by inv_base_step;
+      repeat match goal with
+          |- context [bool_decide ?A] =>
+            destruct (decide A);
+            [rewrite (bool_decide_eq_true_2 A); last done|
+             rewrite (bool_decide_eq_false_2 A); last done]
+        end; simplify_eq/=; auto.
   Local Ltac solve_pure_exec :=
     unfold IntoVal in *;
     repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
@@ -199,8 +208,12 @@ Section lang_rules.
     PureExec True 1 (If (#â™­ false) e1 e2) e2.
   Proof. solve_pure_exec. Qed.
 
-  Global Instance wp_nat_binop op a b :
-    PureExec True 1 (BinOp op (#n a) (#n b)) (of_val (binop_eval op a b)).
+  Global Instance wp_int_binop op a b :
+    PureExec True 1 (BinOp op (#n a) (#n b)) (of_val (int_binop_eval op a b)).
+  Proof. destruct op; solve_pure_exec. Qed.
+
+  Global Instance wp_Eq_binop `{!AsVal e1} `{!AsVal e2} :
+    PureExec True 1 (BinOp Eq e1 e2) (#â™­ (bool_decide (e1 = e2))).
   Proof. solve_pure_exec. Qed.
 
 End lang_rules.