diff --git a/_CoqProject b/_CoqProject
index 50b5c06cdde2b32c4b5735d1cea1f077f881eed5..3bd069d9470d6943ac46dda8fe788ca9f0808f6a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -30,6 +30,7 @@ theories/typing/types.v
 theories/typing/interp.v
 theories/typing/fundamental.v
 theories/typing/contextual_refinement.v
+theories/typing/tactics.v
 theories/typing/soundness.v
 
 theories/reloc.v
diff --git a/theories/examples/or.v b/theories/examples/or.v
index a794d2abd5e0a938cf1550ccede01f6c654df1f6..5ce043a9366f6a899aa865e22120d6f550d5e1e0 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -288,4 +288,75 @@ Section rules.
 
 End rules.
 
-(* TODO: write out the contextual refinements *)
+
+(** Separately, we prove that the ordering induced by âŠ• conincides with
+    contextual refinement. *)
+Lemma Seq_typed Î“ e1 e2 Ï„ :
+  Î“ âŠ¢â‚œ e1 : TUnit â†’
+  Î“ âŠ¢â‚œ e2 : Ï„ â†’
+  Î“ âŠ¢â‚œ (e1;;e2) : Ï„.
+Proof. by repeat (econstructor; eauto). Qed.
+
+Lemma or_equiv_refines_1 e t :
+  (âˆ… âŠ¢â‚œ e : TUnit) â†’
+  (âˆ… âŠ¢â‚œ t : TUnit) â†’
+  (âˆ… âŠ¨ e â‰¤ctxâ‰¤ t : TUnit) â†’
+  (âˆ… âŠ¨ (e âŠ• t) =ctx= t : TUnit).
+Proof.
+  intros Te Tt Het. split; last first.
+  - eapply (ctx_refines_transitive _ _ _ (t âŠ• e)%V).
+    + eapply (refines_sound relocÎ£).
+      iIntros (? Î”).
+      iApply (or_choice_1_r t t  with "[]").
+      by iApply refines_typed.
+    + eapply (refines_sound relocÎ£).
+      iIntros (? Î”). rel_pures_r.
+      iApply or_comm; by iApply (refines_typed TUnit []).
+  - eapply (ctx_refines_transitive _ _ _ (t âŠ• t)%E).
+    + ctx_bind_l e.
+      ctx_bind_r t.
+      eapply (ctx_refines_congruence âˆ… _ _ TUnit);
+        last eassumption.
+      { cbn.
+        econstructor; cbn; eauto.
+        - econstructor; cbn; eauto.
+          econstructor; cbn; eauto.
+        - econstructor; cbn; eauto.
+          + econstructor; cbn; eauto.
+            econstructor; cbn; eauto.
+            econstructor; cbn; eauto.
+            change Z0 with (Z.of_nat 0%nat).
+            econstructor; cbn; eauto.
+            econstructor; cbn; eauto.
+            * econstructor; cbn; eauto.
+              eapply Seq_typed.
+              ** change 1%Z with (Z.of_nat 1%nat).
+                 repeat (econstructor; cbn; eauto).
+              ** repeat (econstructor; cbn; eauto).
+            * repeat (econstructor; cbn; eauto).
+          + econstructor; cbn; eauto.
+            2:{ econstructor; cbn; eauto. }
+            enough (typed_ctx_item (CTX_Rec <> <>)
+                       (binder_insert BAnon (TUnit â†’ TUnit)%ty
+                                      (binder_insert BAnon TUnit (âˆ… : stringmap type)))
+                       TUnit âˆ… (TUnit â†’ TUnit)).
+            { by simpl in *. }
+            eapply (TP_CTX_Rec âˆ… TUnit TUnit BAnon BAnon). }
+    + eapply (refines_sound relocÎ£).
+      iIntros (? Î”). rel_pures_l.
+      iApply or_idemp_l. by iApply (refines_typed TUnit []).
+Qed.
+
+Lemma or_equiv_refines_2 e t :
+  (âˆ… âŠ¢â‚œ e : TUnit) â†’
+  (âˆ… âŠ¢â‚œ t : TUnit) â†’
+  (âˆ… âŠ¨ (e âŠ• t) =ctx= t : TUnit) â†’
+  (âˆ… âŠ¨ e â‰¤ctxâ‰¤ t : TUnit).
+Proof.
+  intros Te Tt [Het1 Het2].
+  eapply (ctx_refines_transitive _ _ _ (e âŠ• t)%E); last assumption.
+  eapply (refines_sound relocÎ£).
+  iIntros (? Î”).
+  rel_pures_r. iApply or_choice_1_r.
+  by iApply (refines_typed TUnit []).
+Qed.
diff --git a/theories/reloc.v b/theories/reloc.v
index 9e4e1d3c796b590fa0204cd3d9b857958ac19edc..fed94d6ead0f73cfecc3d8ae4d0112ce954f3738 100644
--- a/theories/reloc.v
+++ b/theories/reloc.v
@@ -2,4 +2,4 @@ From iris.heap_lang Require Export lang notation proofmode.
 From iris.proofmode Require Export tactics.
 From reloc.logic Require Export proofmode.tactics proofmode.spec_tactics model.
 From reloc.logic Require Export rules derived compatibility.
-From reloc.typing Require Export interp soundness.
+From reloc.typing Require Export interp tactics soundness.
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index c12db48cae684d62a290cb71b4168d6812027a18..74c7248b207387bdcca2c13888a4026033f85986 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -6,14 +6,14 @@ From iris.proofmode Require Import tactics.
 From reloc.typing Require Export types interp fundamental.
 
 Inductive ctx_item :=
-  (* Î»-rec *)
-  | CTX_Rec (f x: binder)
+  (* Base lambda calculus *)
+  | CTX_Rec (f x : binder)
   | CTX_AppL (e2 : expr)
   | CTX_AppR (e1 : expr)
-  (* Bin op *)
+  (* Base types and their operations *)
+  | CTX_UnOp (op : un_op)
   | CTX_BinOpL (op : bin_op) (e2 : expr)
   | CTX_BinOpR (op : bin_op) (e1 : expr)
-  (* If *)
   | CTX_IfL (e1 : expr) (e2 : expr)
   | CTX_IfM (e0 : expr) (e2 : expr)
   | CTX_IfR (e0 : expr) (e1 : expr)
@@ -28,6 +28,19 @@ Inductive ctx_item :=
   | CTX_CaseL (e1 : expr) (e2 : expr)
   | CTX_CaseM (e0 : expr) (e2 : expr)
   | CTX_CaseR (e0 : expr) (e1 : expr)
+  (* Concurrency *)
+  | CTX_Fork
+  (* Heap *)
+  | CTX_Alloc
+  | CTX_Load
+  | CTX_StoreL (e2 : expr)
+  | CTX_StoreR (e1 : expr)
+  (* Compare-exchange and FAA *)
+  | CTX_CmpXchgL (e1 : expr) (e2 : expr)
+  | CTX_CmpXchgM (e0 : expr) (e2 : expr)
+  | CTX_CmpXchgR (e0 : expr) (e1 : expr)
+  | CTX_FAAL (e1 : expr)
+  | CTX_FAAR (e0 : expr)
   (* Recursive Types *)
   | CTX_Fold
   | CTX_Unfold
@@ -35,55 +48,54 @@ Inductive ctx_item :=
   | CTX_TLam
   | CTX_TApp
   (* Existential types *)
-  (* | CTX_Pack *)
-  (* | CTX_UnpackL (e' : expr) *)
-  (* | CTX_UnpackR (e : expr) *)
-  (* Concurrency *)
-  | CTX_Fork
-  (* Reference Types *)
-  | CTX_Alloc
-  | CTX_Load
-  | CTX_StoreL (e2 : expr)
-  | CTX_StoreR (e1 : expr)
-  (* Compare-exchange used for fine-grained concurrency *)
-  | CTX_CmpXchg_L (e1 : expr) (e2 : expr)
-  | CTX_CmpXchg_M (e0 : expr) (e2 : expr)
-  | CTX_CmpXchg_R (e0 : expr) (e1 : expr).
+    (* Nb: we do not have an explicit PACK operation *)
+  | CTX_UnpackL (x : binder) (e2 : expr)
+  | CTX_UnpackR (x : binder) (e1 : expr)
+.
 
 Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
   match ctx with
+  (* Base lambda calculus *)
   | CTX_Rec f x => Rec f x e
   | CTX_AppL e2 => App e e2
   | CTX_AppR e1 => App e1 e
+  (* Base types and operations *)
+  | CTX_UnOp op => UnOp op e
+  | CTX_BinOpL op e2 => BinOp op e e2
+  | CTX_BinOpR op e1 => BinOp op e1 e
+  | CTX_IfL e1 e2 => If e e1 e2
+  | CTX_IfM e0 e2 => If e0 e e2
+  | CTX_IfR e0 e1 => If e0 e1 e
+  (* Products *)
   | CTX_PairL e2 => Pair e e2
   | CTX_PairR e1 => Pair e1 e
   | CTX_Fst => Fst e
   | CTX_Snd => Snd e
+  (* Sums *)
   | CTX_InjL => InjL e
   | CTX_InjR => InjR e
   | CTX_CaseL e1 e2 => Case e e1 e2
   | CTX_CaseM e0 e2 => Case e0 e e2
   | CTX_CaseR e0 e1 => Case e0 e1 e
-  | CTX_BinOpL op e2 => BinOp op e e2
-  | CTX_BinOpR op e1 => BinOp op e1 e
-  | CTX_IfL e1 e2 => If e e1 e2
-  | CTX_IfM e0 e2 => If e0 e e2
-  | CTX_IfR e0 e1 => If e0 e1 e
-  | CTX_Fold => e
-  | CTX_Unfold => rec_unfold e
-  | CTX_TLam => Î›: e
-  | CTX_TApp => TApp e
-  (* | CTX_Pack => Pack e *)
-  (* | CTX_UnpackL e1 => Unpack e e1 *)
-  (* | CTX_UnpackR e0 => Unpack e0 e *)
+  (* Concurrency *)
   | CTX_Fork => Fork e
+  (* Heap & atomic CAS/FAA *)
   | CTX_Alloc => Alloc e
   | CTX_Load => Load e
   | CTX_StoreL e2 => Store e e2
   | CTX_StoreR e1 => Store e1 e
-  | CTX_CmpXchg_L e1 e2 => CmpXchg e e1 e2
-  | CTX_CmpXchg_M e0 e2 => CmpXchg e0 e e2
-  | CTX_CmpXchg_R e0 e1 => CmpXchg e0 e1 e
+  | CTX_CmpXchgL e1 e2 => CmpXchg e e1 e2
+  | CTX_CmpXchgM e0 e2 => CmpXchg e0 e e2
+  | CTX_CmpXchgR e0 e1 => CmpXchg e0 e1 e
+  | CTX_FAAL e1 => FAA e e1
+  | CTX_FAAR e0 => FAA e0 e
+  (* Recursive & polymorphic types *)
+  | CTX_Fold => e
+  | CTX_Unfold => rec_unfold e
+  | CTX_TLam => Î›: e
+  | CTX_TApp => TApp e
+  | CTX_UnpackL x e1 => unpack: x:=e in e1
+  | CTX_UnpackR x e0 => unpack: x:=e0 in e
   end.
 
 Definition ctx := list ctx_item.
@@ -94,6 +106,7 @@ Definition fill_ctx (K : ctx) (e : expr) : expr := foldr fill_ctx_item e K.
 (** typed ctx *)
 Inductive typed_ctx_item :
     ctx_item â†’ stringmap type â†’ type â†’ stringmap type â†’ type â†’ Prop :=
+  (* Base lambda calculus *)
   | TP_CTX_Rec Î“ Ï„ Ï„' f x :
      typed_ctx_item (CTX_Rec f x) (<[f:=TArrow Ï„ Ï„']>(<[x:=Ï„]>Î“)) Ï„' Î“ (TArrow Ï„ Ï„')
   | TP_CTX_AppL Î“ e2 Ï„ Ï„' :
@@ -102,6 +115,33 @@ Inductive typed_ctx_item :
   | TP_CTX_AppR Î“ e1 Ï„ Ï„' :
      typed Î“ e1 (TArrow Ï„ Ï„') â†’
      typed_ctx_item (CTX_AppR e1) Î“ Ï„ Î“ Ï„'
+  (* Base types and operations *)
+  | TP_CTX_BinOpL_Nat op Î“ e2 Ï„ :
+     typed Î“ e2 TNat â†’
+     binop_nat_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpL op e2) Î“ TNat Î“ Ï„
+  | TP_CTX_BinOpR_Nat op e1 Î“ Ï„ :
+     typed Î“ e1 TNat â†’
+     binop_nat_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpR op e1) Î“ TNat Î“ Ï„
+  | TP_CTX_BinOpL_Bool op Î“ e2 Ï„ :
+     typed Î“ e2 TBool â†’
+     binop_bool_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpL op e2) Î“ TBool Î“ Ï„
+  | TP_CTX_BinOpR_Bool op e1 Î“ Ï„ :
+     typed Î“ e1 TBool â†’
+     binop_bool_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpR op e1) Î“ TBool Î“ Ï„
+  | TP_CTX_IfL Î“ e1 e2 Ï„ :
+     typed Î“ e1 Ï„ â†’ typed Î“ e2 Ï„ â†’
+     typed_ctx_item (CTX_IfL e1 e2) Î“ (TBool) Î“ Ï„
+  | TP_CTX_IfM Î“ e0 e2 Ï„ :
+     typed Î“ e0 (TBool) â†’ typed Î“ e2 Ï„ â†’
+     typed_ctx_item (CTX_IfM e0 e2) Î“ Ï„ Î“ Ï„
+  | TP_CTX_IfR Î“ e0 e1 Ï„ :
+     typed Î“ e0 (TBool) â†’ typed Î“ e1 Ï„ â†’
+     typed_ctx_item (CTX_IfR e0 e1) Î“ Ï„ Î“ Ï„
+  (* Products *)
   | TP_CTX_PairL Î“ e2 Ï„ Ï„' :
      typed Î“ e2 Ï„' â†’
      typed_ctx_item (CTX_PairL e2) Î“ Ï„ Î“ (TProd Ï„ Ï„')
@@ -112,6 +152,7 @@ Inductive typed_ctx_item :
      typed_ctx_item CTX_Fst Î“ (TProd Ï„ Ï„') Î“ Ï„
   | TP_CTX_Snd Î“ Ï„ Ï„' :
      typed_ctx_item CTX_Snd Î“ (TProd Ï„ Ï„') Î“ Ï„'
+  (* Sums *)
   | TP_CTX_InjL Î“ Ï„ Ï„' :
      typed_ctx_item CTX_InjL Î“ Ï„ Î“ (TSum Ï„ Ï„')
   | TP_CTX_InjR Î“ Ï„ Ï„' :
@@ -125,49 +166,10 @@ Inductive typed_ctx_item :
   | TP_CTX_CaseR Î“ e0 e1 Ï„1 Ï„2 Ï„' :
      typed Î“ e0 (TSum Ï„1 Ï„2) â†’ typed Î“ e1 (TArrow Ï„1 Ï„') â†’
      typed_ctx_item (CTX_CaseR e0 e1) Î“ (TArrow Ï„2 Ï„') Î“ Ï„'
-  | TP_CTX_IfL Î“ e1 e2 Ï„ :
-     typed Î“ e1 Ï„ â†’ typed Î“ e2 Ï„ â†’
-     typed_ctx_item (CTX_IfL e1 e2) Î“ (TBool) Î“ Ï„
-  | TP_CTX_IfM Î“ e0 e2 Ï„ :
-     typed Î“ e0 (TBool) â†’ typed Î“ e2 Ï„ â†’
-     typed_ctx_item (CTX_IfM e0 e2) Î“ Ï„ Î“ Ï„
-  | TP_CTX_IfR Î“ e0 e1 Ï„ :
-     typed Î“ e0 (TBool) â†’ typed Î“ e1 Ï„ â†’
-     typed_ctx_item (CTX_IfR e0 e1) Î“ Ï„ Î“ Ï„
-  | TP_CTX_BinOpL_Nat op Î“ e2 Ï„ :
-     typed Î“ e2 TNat â†’
-     binop_nat_res_type op = Some Ï„ â†’
-     typed_ctx_item (CTX_BinOpL op e2) Î“ TNat Î“ Ï„
-  | TP_CTX_BinOpR_Nat op e1 Î“ Ï„ :
-     typed Î“ e1 TNat â†’
-     binop_nat_res_type op = Some Ï„ â†’
-     typed_ctx_item (CTX_BinOpR op e1) Î“ TNat Î“ Ï„
-  | TP_CTX_BinOpL_Bool op Î“ e2 Ï„ :
-     typed Î“ e2 TBool â†’
-     binop_bool_res_type op = Some Ï„ â†’
-     typed_ctx_item (CTX_BinOpL op e2) Î“ TBool Î“ Ï„
-  | TP_CTX_BinOpR_Bool op e1 Î“ Ï„ :
-     typed Î“ e1 TBool â†’
-     binop_bool_res_type op = Some Ï„ â†’
-     typed_ctx_item (CTX_BinOpR op e1) Î“ TBool Î“ Ï„
-  | TP_CTX_Fold Î“ Ï„ :
-     typed_ctx_item CTX_Fold Î“ Ï„.[(TRec Ï„)/] Î“ (TRec Ï„)
-  | TP_CTX_Unfold Î“ Ï„ :
-     typed_ctx_item CTX_Unfold Î“ (TRec Ï„) Î“ Ï„.[(TRec Ï„)/]
-  | TP_CTX_TLam Î“ Ï„ :
-     typed_ctx_item CTX_TLam (Autosubst_Classes.subst (ren (+1%nat)) <$> Î“) Ï„ Î“ (TForall Ï„)
-  | TP_CTX_TApp Î“ Ï„ Ï„' :
-     typed_ctx_item CTX_TApp Î“ (TForall Ï„) Î“ Ï„.[Ï„'/]
-  (* | TP_CTX_Pack Î“ Ï„ Ï„' : *)
-  (*    typed_ctx_item CTX_Pack Î“ Ï„.[Ï„'/] Î“ (TExists Ï„) *)
-  (* | TP_CTX_UnpackL e2 Î“ Ï„ Ï„2 : *)
-  (*    typed (subst (ren (+1)) <$> Î“) e2 (TArrow Ï„ (subst (ren (+1)) Ï„2)) â†’ *)
-  (*    typed_ctx_item (CTX_UnpackL e2) Î“ (TExists Ï„) Î“ Ï„2 *)
-  (* | TP_CTX_UnpackR e1 Î“ Ï„ Ï„2 : *)
-  (*    typed Î“ e1 (TExists Ï„) â†’ *)
-  (*    typed_ctx_item (CTX_UnpackR e1) (subst (ren (+1)) <$> Î“) (TArrow Ï„ (subst (ren (+1)) Ï„2))  Î“ Ï„2 *)
+  (* Concurrency *)
   | TP_CTX_Fork Î“ :
      typed_ctx_item CTX_Fork Î“ TUnit Î“ TUnit
+  (* Heap *)
   | TPCTX_Alloc Î“ Ï„ :
      typed_ctx_item CTX_Alloc Î“ Ï„ Î“ (Tref Ï„)
   | TP_CTX_Load Î“ Ï„ :
@@ -177,18 +179,44 @@ Inductive typed_ctx_item :
   | TP_CTX_StoreR Î“ e1 Ï„ :
      typed Î“ e1 (Tref Ï„) â†’
      typed_ctx_item (CTX_StoreR e1) Î“ Ï„ Î“ TUnit
-  | TP_CTX_CasL Î“ e1  e2 Ï„ :
+  | TP_CTX_FAAL Î“ e2 :
+     Î“ âŠ¢â‚œ e2 : TNat â†’
+     typed_ctx_item (CTX_FAAL e2) Î“ (Tref TNat) Î“ TNat
+  | TP_CTX_FAAR Î“ e1 :
+     Î“ âŠ¢â‚œ e1 : Tref TNat â†’
+     typed_ctx_item (CTX_FAAR e1) Î“ TNat Î“ TNat
+  | TP_CTX_CasL Î“ e1 e2 Ï„ :
      EqType Ï„ â†’ UnboxedType Ï„ â†’
      typed Î“ e1 Ï„ â†’ typed Î“ e2 Ï„ â†’
-     typed_ctx_item (CTX_CmpXchg_L e1 e2) Î“ (Tref Ï„) Î“ (TProd Ï„ TBool)
+     typed_ctx_item (CTX_CmpXchgL e1 e2) Î“ (Tref Ï„) Î“ (TProd Ï„ TBool)
   | TP_CTX_CasM Î“ e0 e2 Ï„ :
      EqType Ï„ â†’ UnboxedType Ï„ â†’
      typed Î“ e0 (Tref Ï„) â†’ typed Î“ e2 Ï„ â†’
-     typed_ctx_item (CTX_CmpXchg_M e0 e2) Î“ Ï„ Î“ (TProd Ï„ TBool)
+     typed_ctx_item (CTX_CmpXchgM e0 e2) Î“ Ï„ Î“ (TProd Ï„ TBool)
   | TP_CTX_CasR Î“ e0 e1 Ï„ :
      EqType Ï„ â†’ UnboxedType Ï„ â†’
      typed Î“ e0 (Tref Ï„) â†’ typed Î“ e1 Ï„ â†’
-     typed_ctx_item (CTX_CmpXchg_R e0 e1) Î“ Ï„ Î“ (TProd Ï„ TBool).
+     typed_ctx_item (CTX_CmpXchgR e0 e1) Î“ Ï„ Î“ (TProd Ï„ TBool)
+  (* Polymorphic & recursive types *)
+  | TP_CTX_Fold Î“ Ï„ :
+     typed_ctx_item CTX_Fold Î“ Ï„.[(TRec Ï„)/] Î“ (TRec Ï„)
+  | TP_CTX_Unfold Î“ Ï„ :
+     typed_ctx_item CTX_Unfold Î“ (TRec Ï„) Î“ Ï„.[(TRec Ï„)/]
+  | TP_CTX_TLam Î“ Ï„ :
+     typed_ctx_item CTX_TLam (Autosubst_Classes.subst (ren (+1%nat)) <$> Î“) Ï„ Î“ (TForall Ï„)
+  | TP_CTX_TApp Î“ Ï„ Ï„' :
+     typed_ctx_item CTX_TApp Î“ (TForall Ï„) Î“ Ï„.[Ï„'/]
+  (* | TP_CTX_Pack Î“ Ï„ Ï„' : *)
+  (*    typed_ctx_item CTX_Pack Î“ Ï„.[Ï„'/] Î“ (TExists Ï„) *)
+  | TP_CTX_UnpackL x e2 Î“ Ï„ Ï„2 :
+     <[x:=Ï„]>(â¤‰ Î“) âŠ¢â‚œ e2 : (Autosubst_Classes.subst (ren (+1%nat)) Ï„2) â†’
+     typed_ctx_item (CTX_UnpackL x e2) Î“ (TExists Ï„) Î“ Ï„2
+  | TP_CTX_UnpackR x e1 Î“ Ï„ Ï„2 :
+      Î“ âŠ¢â‚œ e1 : TExists Ï„ â†’
+     typed_ctx_item (CTX_UnpackR x e1)
+                    (<[x:=Ï„]>(â¤‰ Î“)) (Autosubst_Classes.subst (ren (+1%nat)) Ï„2)
+                    Î“ Ï„2
+.
 
 Inductive typed_ctx: ctx â†’ stringmap type â†’ type â†’ stringmap type â†’ type â†’ Prop :=
   | TPCTX_nil Î“ Ï„ :
@@ -263,6 +291,14 @@ Proof.
   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 Î£}.
 
@@ -288,6 +324,27 @@ Section bin_log_related_under_typed_ctx.
       + iApply (bin_log_related_app _ _ _ _ _ _ Ï„2 with "[]").
         by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_nat_binop with "[]");
+          try (by iApply fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_nat_binop with "[]");
+          try (by iApply fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_bool_binop with "[]");
+          try (by iApply fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_bool_binop with "[]");
+          try (by iApply fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_if with "[] []");
+          try by iApply fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_if with "[] []");
+          try by iApply fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_if with "[] []");
+          try by iApply fundamental.
+        iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_pair with "[]").
         iApply (IHK with "[Hrel]"); auto.
         by iApply fundamental.
@@ -314,42 +371,6 @@ Section bin_log_related_under_typed_ctx.
         by iApply fundamental.
         by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_if with "[] []");
-          try by iApply fundamental.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_if with "[] []");
-          try by iApply fundamental.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_if with "[] []");
-          try by iApply fundamental.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_nat_binop with "[]");
-          try (by iApply fundamental); eauto.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_nat_binop with "[]");
-          try (by iApply fundamental); eauto.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_bool_binop with "[]");
-          try (by iApply fundamental); eauto.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_bool_binop with "[]");
-          try (by iApply fundamental); eauto.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_fold with "[]").
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_unfold with "[]").
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_tlam with "[]").
-        iIntros (Ï„i). iAlways.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_tapp' with "[]").
-        iApply (IHK with "[Hrel]"); auto.
-      (* + iApply bin_log_related_pack'. *)
-      (*   iApply (IHK with "[Hrel]"); auto. *)
-      (* + iApply bin_log_related_unpack; try by (iIntros; fundamental). *)
-      (*   iApply (IHK with "[Hrel]"); auto. *)
-      (* + iApply bin_log_related_unpack; try by (iIntros; fundamental). *)
-      (*   iIntros. iApply (IHK with "[Hrel]"); auto. *)
       + iApply (bin_log_related_fork with "[]").
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_alloc with "[]").
@@ -362,6 +383,12 @@ Section bin_log_related_under_typed_ctx.
       + iApply (bin_log_related_store with "[]");
           try by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
+      + iApply bin_log_related_FAA;
+          try (by iApply fundamental); eauto.
+        iApply (IHK with "Hrel").
+      + iApply bin_log_related_FAA;
+          try (by iApply fundamental); eauto.
+        iApply (IHK with "Hrel").
       + iApply (bin_log_related_CmpXchg with "[] []");
           try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
@@ -371,5 +398,20 @@ Section bin_log_related_under_typed_ctx.
       + iApply (bin_log_related_CmpXchg with "[] []");
           try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_fold with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_unfold with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_tlam with "[]").
+        iIntros (Ï„i). iAlways.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_tapp' with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply bin_log_related_unpack.
+        * iApply (IHK with "[Hrel]"); auto.
+        * iIntros (A). by iApply fundamental.
+      + iApply bin_log_related_unpack.
+        * by iApply fundamental.
+        * iIntros (A). iApply (IHK with "[Hrel]"); auto.
   Qed.
 End bin_log_related_under_typed_ctx.
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 4b2d7e8a998e86938e4a5a4997453983c32fce6b..74d4d01800a09d9d3cea6cd26e065431ed2127ca 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -274,6 +274,29 @@ Section fundamental.
     - by iApply "IH2".
   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.
+  Proof.
+    iIntros "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 (l l') "(% & % & Hinv)"; simplify_eq/=.
+    iDestruct "IH2" as (n) "[% %]". simplify_eq.
+    rel_apply_l refines_faa_l.
+    iInv (relocN .@ "ref" .@ (l,l')) as (v1 v1') "[Hv1 [>Hv2 #>Hv]]" "Hclose".
+    iDestruct "Hv" as (n1) "[% %]"; simplify_eq.
+    iModIntro. iExists _; iFrame. iNext.
+    iIntros "Hl".
+    (* TODO: tactics for these operations *)
+    rel_apply_r (refines_faa_r with "Hv2"). iIntros "Hv2".
+    iMod ("Hclose" with "[-]") as "_".
+    { iNext. iExists _,_. iFrame. iExists _; iSplit; eauto. }
+    rel_values.
+  Qed.
+
   Lemma bin_log_related_CmpXchg Î” Î“ e1 e2 e3 e1' e2' e3' Ï„
     (HEqÏ„ : EqType Ï„)
     (HUbÏ„ : UnboxedType Ï„) :
@@ -518,6 +541,8 @@ Section fundamental.
       + iApply bin_log_related_alloc; by iApply fundamental.
       + iApply bin_log_related_load; by iApply fundamental.
       + iApply bin_log_related_store; by iApply fundamental.
+      + iApply bin_log_related_FAA; eauto;
+          by iApply fundamental.
       + iApply bin_log_related_CmpXchg; eauto;
           by iApply fundamental.
     - intros Hv. destruct Hv; simpl.
diff --git a/theories/typing/tactics.v b/theories/typing/tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..817fb070dfe58413119ab477df56fc57b8a67643
--- /dev/null
+++ b/theories/typing/tactics.v
@@ -0,0 +1,84 @@
+From reloc.typing Require Export types contextual_refinement.
+
+Lemma tac_ctx_bind_l e' C Î“ e t Ï„ :
+  e = fill_ctx C e' â†’
+  ctx_refines Î“ (fill_ctx C e') t Ï„ â†’
+  ctx_refines Î“ e t Ï„.
+Proof. intros; subst; assumption. Qed.
+
+Lemma tac_ctx_bind_r e' C Î“ e t Ï„ :
+  e = fill_ctx C e' â†’
+  ctx_refines Î“ t (fill_ctx C e') Ï„ â†’
+  ctx_refines Î“ t e Ï„.
+Proof. intros; subst; assumption. Qed.
+
+Ltac reshape_expr_ctx e tac :=
+  let rec go K e :=
+    match e with
+    | _                     => tac (reverse K) e
+    (* Base lambda calculus *)
+
+    | Rec ?f ?x ?e          => add_item (CTX_Rec f x) K e
+    | App ?e1 ?e2           => add_item (CTX_AppL e2) K e1
+    | App ?e1 ?e2           => add_item (CTX_AppR e1) K e2
+    (* Base types and their operations *)
+    | UnOp ?op ?e           => add_item (UnOpCtx op) K e
+    | BinOp ?op ?e1 ?e2     => add_item (CTX_BinOpL op e2) K e1
+    | BinOp ?op ?e1 ?e2     => add_item (CTX_BinOpR op e1) K e2
+    | If ?e0 ?e1 ?e2        => add_item (CTX_IfL e1 e2) K e0
+    | If ?e0 ?e1 ?e2        => add_item (CTX_IfM e0 e2) K e1
+    | If ?e0 ?e1 ?e2        => add_item (CTX_IfR e0 e1) K e2
+    (* Products *)
+    | Pair ?e1 ?e2          => add_item (CTX_PairL e2) K e1
+    | Pair ?e1 ?e2          => add_item (CTX_PairR e1) K e2
+    | Fst ?e                => add_item CTX_Fst K e
+    | Snd ?e                => add_item CTX_Snd K e
+    (* Sums *)
+    | InjL ?e               => add_item CTX_InjL K e
+    | InjR ?e               => add_item CTX_InjR K e
+    | Case ?e0 ?e1 ?e2      => add_item (CTX_CaseL e1 e2) K e0
+    | Case ?e0 ?e1 ?e2      => add_item (CTX_CaseM e0 e2) K e1
+    | Case ?e0 ?e1 ?e2      => add_item (CTX_CaseR e0 e1) K e2
+    (* Concurrency *)
+    | Fork ?e               => add_item CTX_Fork K e
+    (* Heap *)
+    | Alloc  ?e             => add_item CTX_Alloc K e
+    | Load ?e               => add_item CTX_Load K e
+    | Store ?e1 ?e2         => add_item (CTX_StoreR e1) K e2
+    | Store ?e1 ?e2         => add_item (CTX_StoreL e2) K e1
+    (* Compare-exchange *)
+    | CmpXchg ?e0 ?e1 ?e2   => add_item (CTX_CmpXchgL e1 e2) K e0
+    | CmpXchg ?e0 ?e1 ?e2   => add_item (CTX_CmpXchgM e0 e2) K e1
+    | CmpXchg ?e0 ?e1 ?e2   => add_item (CTX_CmpXchgR e0 e1) K e2
+    | FAA ?e0 ?e1           => add_item (CTX_FAAL e1) K e0
+    | FAA ?e0 ?e1           => add_item (CTX_FAAR e0) K e1
+    end
+  with add_item Ki K e := go (Ki :: K) e
+  in
+  go (@nil ctx_item) e.
+
+Ltac ctx_bind_helper :=
+  simpl;
+  lazymatch goal with
+  | |- fill_ctx ?K ?e = fill_ctx _ ?efoc =>
+     reshape_expr_ctx e ltac:(fun K' e' =>
+       unify e' efoc;
+       let K'' := eval cbn[app] in (K' ++ K) in
+       replace (fill_ctx K e) with (fill_ctx K'' e') by (by rewrite ?fill_ctx_app))
+  | |- ?e = fill_ctx _ ?efoc =>
+     reshape_expr_ctx e ltac:(fun K' e' =>
+       unify e' efoc;
+       replace e with (fill_ctx K' e') by (by rewrite ?fill_ctx_app))
+  end; reflexivity.
+
+Tactic Notation "ctx_bind_l" open_constr(efoc) :=
+  eapply (tac_ctx_bind_l efoc);
+  [ ctx_bind_helper
+  | (* new goal *)
+  ].
+
+Tactic Notation "ctx_bind_r" open_constr(efoc) :=
+  eapply (tac_ctx_bind_r efoc);
+  [ ctx_bind_helper
+  | (* new goal *)
+  ].
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 64f5f1ac0a274a9ddf8b9d976a180bdcf5ac4d8c..c94c6d6c02f748c6b0f4231415d6b07173ceafcf 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -106,9 +106,12 @@ Inductive typed : stringmap type â†’ expr â†’ type â†’ Prop :=
   | Val_typed Î“ v Ï„ :
       âŠ¢áµ¥ v : Ï„ â†’
       Î“ âŠ¢â‚œ Val v : Ï„
-  | Unit_typed Î“ : Î“ âŠ¢â‚œ #() : TUnit
-  | Nat_typed Î“ (n : nat) : Î“ âŠ¢â‚œ # n : TNat
-  | Bool_typed Î“ (b : bool) : Î“ âŠ¢â‚œ # b : TBool
+  | Unit_typed Î“ :
+      Î“ âŠ¢â‚œ #() : TUnit
+  | Nat_typed Î“ (n : nat) :
+      Î“ âŠ¢â‚œ #n : TNat
+  | Bool_typed Î“ (b : bool) :
+      Î“ âŠ¢â‚œ #b : TBool
   | BinOp_typed_nat Î“ op e1 e2 Ï„ :
      Î“ âŠ¢â‚œ e1 : TNat â†’ Î“ âŠ¢â‚œ e2 : TNat â†’
      binop_nat_res_type op = Some Ï„ â†’
@@ -120,39 +123,65 @@ Inductive typed : stringmap type â†’ expr â†’ type â†’ Prop :=
   | RefEq_typed Î“ e1 e2 Ï„ :
      Î“ âŠ¢â‚œ e1 : Tref Ï„ â†’ Î“ âŠ¢â‚œ e2 : Tref Ï„ â†’
      Î“ âŠ¢â‚œ BinOp EqOp 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
-  | InjR_typed Î“ e Ï„1 Ï„2 : Î“ âŠ¢â‚œ e : Ï„2 â†’ Î“ âŠ¢â‚œ InjR e : TSum Ï„1 Ï„2
+  | Pair_typed Î“ e1 e2 Ï„1 Ï„2 :
+      Î“ âŠ¢â‚œ e1 : Ï„1 â†’ Î“ âŠ¢â‚œ e2 : Ï„2 â†’
+      Î“ âŠ¢â‚œ (e1, e2) : Ï„1 * Ï„2
+  | Fst_typed Î“ e Ï„1 Ï„2 :
+      Î“ âŠ¢â‚œ e : Ï„1 * Ï„2 â†’
+      Î“ âŠ¢â‚œ Fst e : Ï„1
+  | Snd_typed Î“ e Ï„1 Ï„2 :
+      Î“ âŠ¢â‚œ e : Ï„1 * Ï„2 â†’
+      Î“ âŠ¢â‚œ Snd e : Ï„2
+  | InjL_typed Î“ e Ï„1 Ï„2 :
+      Î“ âŠ¢â‚œ e : Ï„1 â†’
+      Î“ âŠ¢â‚œ InjL e : Ï„1 + Ï„2
+  | InjR_typed Î“ e Ï„1 Ï„2 :
+      Î“ âŠ¢â‚œ e : Ï„2 â†’
+      Î“ âŠ¢â‚œ InjR e : Ï„1 + Ï„2
   | Case_typed Î“ e0 e1 e2 Ï„1 Ï„2 Ï„3 :
-     Î“ âŠ¢â‚œ e0 : TSum Ï„1 Ï„2 â†’
-     Î“ âŠ¢â‚œ e1 : TArrow Ï„1 Ï„3 â†’
-     Î“ âŠ¢â‚œ e2 : TArrow Ï„2 Ï„3 â†’
+     Î“ âŠ¢â‚œ e0 : Ï„1 + Ï„2 â†’
+     Î“ âŠ¢â‚œ e1 : (Ï„1 â†’ Ï„3) â†’
+     Î“ âŠ¢â‚œ e2 : (Ï„2 â†’ Ï„3) â†’
      Î“ âŠ¢â‚œ Case e0 e1 e2 : Ï„3
   | If_typed Î“ e0 e1 e2 Ï„ :
-     Î“ âŠ¢â‚œ e0 : TBool â†’ Î“ âŠ¢â‚œ e1 : Ï„ â†’ Î“ âŠ¢â‚œ e2 : Ï„ â†’ Î“ âŠ¢â‚œ If e0 e1 e2 : Ï„
+     Î“ âŠ¢â‚œ e0 : TBool â†’
+     Î“ âŠ¢â‚œ e1 : Ï„ â†’
+     Î“ âŠ¢â‚œ e2 : Ï„ â†’
+     Î“ âŠ¢â‚œ If e0 e1 e2 : Ï„
   | Rec_typed Î“ f x e Ï„1 Ï„2 :
-     <[f:=TArrow Ï„1 Ï„2]>(<[x:=Ï„1]>Î“) âŠ¢â‚œ e : Ï„2 â†’
-     Î“ âŠ¢â‚œ Rec f x e : TArrow Ï„1 Ï„2
+     <[f:=(Ï„1 â†’ Ï„2)%ty]>(<[x:=Ï„1]>Î“) âŠ¢â‚œ e : Ï„2 â†’
+     Î“ âŠ¢â‚œ (rec: f x := e) : (Ï„1 â†’ Ï„2)
   | App_typed Î“ e1 e2 Ï„1 Ï„2 :
-     Î“ âŠ¢â‚œ e1 : TArrow Ï„1 Ï„2 â†’ Î“ âŠ¢â‚œ e2 : Ï„1 â†’ Î“ âŠ¢â‚œ App e1 e2 : Ï„2
+     Î“ âŠ¢â‚œ e1 : (Ï„1 â†’ Ï„2) â†’
+     Î“ âŠ¢â‚œ e2 : Ï„1 â†’
+     Î“ âŠ¢â‚œ e1 e2 : Ï„2
   | TLam_typed Î“ e Ï„ :
      â¤‰ Î“ âŠ¢â‚œ e : Ï„ â†’
-     Î“ âŠ¢â‚œ (Î›: e) : TForall Ï„
-  | TApp_typed Î“ e Ï„ Ï„' : Î“ âŠ¢â‚œ e : TForall Ï„ â†’
+     Î“ âŠ¢â‚œ (Î›: e) : âˆ€: Ï„
+  | TApp_typed Î“ e Ï„ Ï„' :
+     Î“ âŠ¢â‚œ e : (âˆ€: Ï„) â†’
      Î“ âŠ¢â‚œ e #() : Ï„.[Ï„'/]
-  | TFold Î“ e Ï„ : Î“ âŠ¢â‚œ e : Ï„.[TRec Ï„/] â†’ Î“ âŠ¢â‚œe : TRec Ï„
-  | TUnfold Î“ e Ï„ : Î“ âŠ¢â‚œ e : TRec Ï„ â†’ Î“ âŠ¢â‚œ rec_unfold e : Ï„.[TRec Ï„/]
-  | TPack Î“ e Ï„ Ï„' : Î“ âŠ¢â‚œ e : Ï„.[Ï„'/] â†’ Î“ âŠ¢â‚œ e : TExists Ï„
+  | TFold Î“ e Ï„ :
+      Î“ âŠ¢â‚œ e : Ï„.[(Î¼: Ï„)%ty/] â†’
+      Î“ âŠ¢â‚œ e : (Î¼: Ï„)
+  | TUnfold Î“ e Ï„ :
+      Î“ âŠ¢â‚œ e : (Î¼: Ï„)%ty â†’
+      Î“ âŠ¢â‚œ rec_unfold e : Ï„.[(Î¼: Ï„)%ty/]
+  | TPack Î“ e Ï„ Ï„' :
+      Î“ âŠ¢â‚œ e : Ï„.[Ï„'/] â†’
+      Î“ âŠ¢â‚œ e : (âˆƒ: Ï„)
   | TUnpack Î“ e1 x e2 Ï„ Ï„2 :
-      Î“ âŠ¢â‚œ e1 : TExists Ï„ â†’
+      Î“ âŠ¢â‚œ e1 : (âˆƒ: Ï„) â†’
       <[x:=Ï„]>(â¤‰ Î“) âŠ¢â‚œ e2 : (Autosubst_Classes.subst (ren (+1%nat)) Ï„2) â†’
       Î“ âŠ¢â‚œ (unpack: x := e1 in e2) : Ï„2
   | TFork Î“ e : Î“ âŠ¢â‚œ e : TUnit â†’ Î“ âŠ¢â‚œ Fork e : TUnit
   | TAlloc Î“ e Ï„ : Î“ âŠ¢â‚œ e : Ï„ â†’ Î“ âŠ¢â‚œ Alloc e : Tref Ï„
   | TLoad Î“ e Ï„ : Î“ âŠ¢â‚œ e : Tref Ï„ â†’ Î“ âŠ¢â‚œ Load e : Ï„
   | TStore Î“ e e' Ï„ : Î“ âŠ¢â‚œ e : Tref Ï„ â†’ Î“ âŠ¢â‚œ e' : Ï„ â†’ Î“ âŠ¢â‚œ Store e e' : TUnit
+  | TFAA Î“ e1 e2 :
+     Î“ âŠ¢â‚œ e1 : Tref TNat â†’
+     Î“ âŠ¢â‚œ e2 : TNat â†’
+     Î“ âŠ¢â‚œ FAA e1 e2 : TNat
   | TCmpXchg Î“ e1 e2 e3 Ï„ :
      EqType Ï„ â†’ UnboxedType Ï„ â†’
      Î“ âŠ¢â‚œ e1 : Tref Ï„ â†’ Î“ âŠ¢â‚œ e2 : Ï„ â†’ Î“ âŠ¢â‚œ e3 : Ï„ â†’