diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 7ff8d31cb7f62e7f3d4ca8e6094d8cb2e3364817..c12db48cae684d62a290cb71b4168d6812027a18 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -88,6 +88,7 @@ Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
 
 Definition ctx := list ctx_item.
 
+(* TODO: consider using foldl here *)
 Definition fill_ctx (K : ctx) (e : expr) : expr := foldr fill_ctx_item e K.
 
 (** typed ctx *)
@@ -283,15 +284,15 @@ Section bin_log_related_under_typed_ctx.
         iAlways. iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_app with "[]").
         iApply (IHK with "[Hrel]"); auto.
-        by iApply binary_fundamental.
+        by iApply fundamental.
       + iApply (bin_log_related_app _ _ _ _ _ _ Ï„2 with "[]").
-        by iApply binary_fundamental.
+        by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_pair with "[]").
         iApply (IHK with "[Hrel]"); auto.
-        by iApply binary_fundamental.
+        by iApply fundamental.
       + iApply (bin_log_related_pair with "[]").
-        by iApply binary_fundamental.
+        by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply bin_log_related_fst.
         iApply (IHK with "[Hrel]"); auto.
@@ -303,36 +304,36 @@ Section bin_log_related_under_typed_ctx.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_case with "[] []").
         iApply (IHK with "[Hrel]"); auto.
-        by iApply binary_fundamental.
-        by iApply binary_fundamental.
+        by iApply fundamental.
+        by iApply fundamental.
       + iApply (bin_log_related_case with "[] []").
-        by iApply binary_fundamental.
+        by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
-        by iApply binary_fundamental.
+        by iApply fundamental.
       + iApply (bin_log_related_case with "[] []").
-        by iApply binary_fundamental.
-        by iApply binary_fundamental.
+        by iApply fundamental.
+        by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_if with "[] []");
-          try by iApply binary_fundamental.
+          try by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_if with "[] []");
-          try by iApply binary_fundamental.
+          try by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_if with "[] []");
-          try by iApply binary_fundamental.
+          try by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_nat_binop with "[]");
-          try (by iApply binary_fundamental); eauto.
+          try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_nat_binop with "[]");
-          try (by iApply binary_fundamental); eauto.
+          try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_bool_binop with "[]");
-          try (by iApply binary_fundamental); eauto.
+          try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_bool_binop with "[]");
-          try (by iApply binary_fundamental); eauto.
+          try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_fold with "[]").
         iApply (IHK with "[Hrel]"); auto.
@@ -356,19 +357,19 @@ Section bin_log_related_under_typed_ctx.
       + iApply (bin_log_related_load with "[]").
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_store with "[]");
-          try by iApply binary_fundamental.
+          try by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_store with "[]");
-          try by iApply binary_fundamental.
+          try by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_CmpXchg with "[] []");
-          try (by iApply binary_fundamental); eauto.
+          try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_CmpXchg with "[] []");
-          try (by iApply binary_fundamental); eauto.
+          try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_CmpXchg with "[] []");
-          try (by iApply binary_fundamental); eauto.
+          try (by iApply fundamental); eauto.
         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 f583c71d40b16e0a1bae56f890cbe70d91f5e80b..f11af98266db1df978ae5f012d371115acb64670 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -470,44 +470,91 @@ Section fundamental.
     asimpl. eauto.
   Qed.
 
-  Theorem binary_fundamental Δ Γ e τ :
-    Γ ⊢ₜ e : τ → ({Δ;Γ} ⊨ e ≤log≤ e : τ)%I.
+  Theorem fundamental Δ Γ e τ :
+    Γ ⊢ₜ e : τ → ({Δ;Γ} ⊨ e ≤log≤ e : τ)%I
+  with fundamental_val Δ v τ :
+    ⊢ᵥ v : τ → (interp τ Δ v v).
   Proof.
-    intros Ht. iInduction Ht as [] "IH" forall (Δ).
-    - by iApply bin_log_related_var.
-    - iApply bin_log_related_unit.
-    - by iApply bin_log_related_nat.
-    - by iApply bin_log_related_bool.
-    - by iApply (bin_log_related_nat_binop with "[]").
-    - by iApply (bin_log_related_bool_binop with "[]").
-    - by iApply bin_log_related_ref_binop.
-    - by iApply (bin_log_related_pair with "[]").
-    - by iApply bin_log_related_fst.
-    - by iApply bin_log_related_snd.
-    - by iApply bin_log_related_injl.
-    - by iApply bin_log_related_injr.
-    - by iApply (bin_log_related_case with "[] []").
-    - by iApply (bin_log_related_if with "[] []").
-    - iApply (bin_log_related_rec with "[]"); eauto.
-    - by iApply (bin_log_related_app with "[] []").
-    - iApply bin_log_related_tlam; eauto.
-    - by iApply bin_log_related_tapp'.
-    - by iApply bin_log_related_fold.
-    - by iApply bin_log_related_unfold.
-    - by iApply bin_log_related_pack'.
-    - iApply (bin_log_related_unpack with "[]"); eauto.
-    - by iApply bin_log_related_fork.
-    - by iApply bin_log_related_alloc.
-    - by iApply bin_log_related_load.
-    - by iApply (bin_log_related_store with "[]").
-    - by iApply (bin_log_related_CmpXchg with "[] []").
+    - intros Ht. destruct Ht.
+      + by iApply bin_log_related_var.
+      + iIntros (γ) "#H". simpl. rel_values.
+        iModIntro. by iApply fundamental_val.
+      + iApply bin_log_related_unit.
+      + by iApply bin_log_related_nat.
+      + by iApply bin_log_related_bool.
+      + iApply bin_log_related_nat_binop; first done;
+          by iApply fundamental.
+      + iApply bin_log_related_bool_binop; first done;
+          by iApply fundamental.
+      + iApply bin_log_related_ref_binop;
+          by iApply fundamental.
+      + iApply bin_log_related_pair;
+          by iApply fundamental.
+      + iApply bin_log_related_fst;
+          by iApply fundamental.
+      + iApply bin_log_related_snd;
+          by iApply fundamental.
+      + iApply bin_log_related_injl;
+          by iApply fundamental.
+      + iApply bin_log_related_injr;
+          by iApply fundamental.
+      + iApply bin_log_related_case;
+          by iApply fundamental.
+      + iApply bin_log_related_if;
+          by iApply fundamental.
+      + iApply bin_log_related_rec.
+        iAlways. by iApply fundamental.
+      + iApply bin_log_related_app;
+          by iApply fundamental.
+      + iApply bin_log_related_tlam.
+        iIntros (A). iAlways. by iApply fundamental.
+      + iApply bin_log_related_tapp'; by iApply fundamental.
+      + iApply bin_log_related_fold; by iApply fundamental.
+      + iApply bin_log_related_unfold; by iApply fundamental.
+      + iApply bin_log_related_pack'; by iApply fundamental.
+      + iApply bin_log_related_unpack; try by iApply fundamental.
+        iIntros (A). by iApply fundamental.
+      + iApply bin_log_related_fork; by iApply 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_CmpXchg; eauto;
+          by iApply fundamental.
+    - intros Hv. destruct Hv; simpl.
+      + iSplit; eauto.
+      + iExists _; iSplit; eauto.
+      + iExists _; iSplit; eauto.
+      + iExists _,_,_,_.
+        repeat iSplit; eauto; by iApply fundamental_val.
+      + iExists _,_. iLeft.
+        repeat iSplit; eauto; by iApply fundamental_val.
+      + iExists _,_. iRight.
+        repeat iSplit; eauto; by iApply fundamental_val.
+      + iLöb as "IH". iAlways.
+        iIntros (v1 v2) "#Hv".
+        pose (Γ := (<[f:=(τ1 → τ2)%ty]> (<[x:=τ1]> ∅)):stringmap type).
+        pose (γ := (binder_insert f ((rec: f x := e)%V,(rec: f x := e)%V)
+                     (binder_insert x (v1, v2) ∅)):stringmap (val*val)).
+        rel_pure_l. rel_pure_r.
+        iPoseProof (fundamental Δ Γ e τ2 $! γ with "[]") as "H"; eauto.
+        { rewrite /γ /Γ. rewrite !binder_insert_fmap fmap_empty.
+          iApply (env_ltyped2_insert with "IH").
+          iApply (env_ltyped2_insert with "Hv").
+          iApply env_ltyped2_empty. }
+        rewrite /γ /=. rewrite !binder_insert_fmap !fmap_empty /=.
+        by rewrite !subst_map_binder_insert_2_empty.
+      + iIntros (A). iAlways. iIntros (v1 v2) "_".
+        rel_pures_l. rel_pures_r.
+        iPoseProof (fundamental (A::Δ) ∅ e τ $! ∅ with "[]") as "H"; eauto.
+        { rewrite fmap_empty. iApply env_ltyped2_empty. }
+        by rewrite !fmap_empty subst_map_empty.
   Qed.
 
   Theorem refines_typed τ Δ e :
     ∅ ⊢ₜ e : τ →
     REL e << e : (interp τ Δ ).
   Proof.
-    move=> /binary_fundamental Hty.
+    move=> /fundamental Hty.
     iPoseProof (Hty Δ with "[]") as "H".
     { rewrite fmap_empty. iApply env_ltyped2_empty. }
     by rewrite !fmap_empty !subst_map_empty.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 5a22da8f8e5b11524e6fb2ff0966bc3d1656648f..46475a29068edbd7553a88c2b34bf2c5ce95e183 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -41,7 +41,7 @@ Theorem F_mu_ref_conc_typesfety e e' τ σ thp σ' :
 Proof.
   intros.
   eapply (logrel_typesafety relocΣ); eauto.
-  intros. by apply binary_fundamental.
+  intros. by apply fundamental.
 Qed.
 
 Lemma logrel_simul Σ `{relocPreG Σ}
diff --git a/theories/typing/types.v b/theories/typing/types.v
index b2fa1d2bd56d6a43990e9650b14921d536ccc6be..64f5f1ac0a274a9ddf8b9d976a180bdcf5ac4d8c 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -72,6 +72,7 @@ Notation "'ref' Ï„" := (Tref Ï„%ty) (at level 10, Ï„ at next level, right associ
 
 (** * Typing judgements *)
 Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
+Reserved Notation "⊢ᵥ v : τ" (at level 20, v, τ at next level).
 
 (* Shift all the indices in the context by one,
    used when inserting a new type interpretation in Δ. *)
@@ -100,60 +101,84 @@ Instance insert_binder (A : Type): Insert binder A (stringmap A) :=
   binder_insert.
 
 (** Typing itself *)
-Inductive typed (Γ : stringmap type) : expr → type → Prop :=
-  | Var_typed x τ : Γ !! x = Some τ → Γ ⊢ₜ Var x : τ
-  | Unit_typed : Γ ⊢ₜ #() : TUnit
-  | Nat_typed (n : nat) : Γ ⊢ₜ # n : TNat
-  | Bool_typed (b : bool) : Γ ⊢ₜ # b : TBool
-  | BinOp_typed_nat op e1 e2 Ï„ :
+Inductive typed : stringmap type → expr → type → Prop :=
+  | Var_typed Γ x τ : Γ !! x = Some τ → Γ ⊢ₜ Var x : τ
+  | Val_typed Γ v τ :
+      ⊢ᵥ v : τ →
+      Γ ⊢ₜ Val v : τ
+  | 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 τ →
      Γ ⊢ₜ BinOp op e1 e2 : τ
-  | BinOp_typed_bool op e1 e2 Ï„ :
+  | BinOp_typed_bool Γ op e1 e2 τ :
      Γ ⊢ₜ e1 : TBool → Γ ⊢ₜ e2 : TBool →
      binop_bool_res_type op = Some τ →
      Γ ⊢ₜ BinOp op e1 e2 : τ
-  | RefEq_typed e1 e2 Ï„ :
+  | 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
-  | Case_typed e0 e1 e2 Ï„1 Ï„2 Ï„3 :
+  | 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
+  | Case_typed Γ e0 e1 e2 τ1 τ2 τ3 :
      Γ ⊢ₜ e0 : TSum τ1 τ2 →
      Γ ⊢ₜ e1 : TArrow τ1 τ3 →
      Γ ⊢ₜ e2 : TArrow τ2 τ3 →
      Γ ⊢ₜ Case e0 e1 e2 : τ3
-  | If_typed e0 e1 e2 Ï„ :
+  | If_typed Γ e0 e1 e2 τ :
      Γ ⊢ₜ e0 : TBool → Γ ⊢ₜ e1 : τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ If e0 e1 e2 : τ
-  | Rec_typed f x e Ï„1 Ï„2 :
+  | Rec_typed Γ f x e τ1 τ2 :
      <[f:=TArrow τ1 τ2]>(<[x:=τ1]>Γ) ⊢ₜ e : τ2 →
      Γ ⊢ₜ Rec f x e : TArrow τ1 τ2
-  | App_typed e1 e2 Ï„1 Ï„2 :
+  | App_typed Γ e1 e2 τ1 τ2 :
      Γ ⊢ₜ e1 : TArrow τ1 τ2 → Γ ⊢ₜ e2 : τ1 → Γ ⊢ₜ App e1 e2 : τ2
-  | TLam_typed e Ï„ :
+  | TLam_typed Γ e τ :
      ⤉ Γ ⊢ₜ e : τ →
      Γ ⊢ₜ (Λ: e) : TForall τ
-  | TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ →
+  | TApp_typed Γ e τ τ' : Γ ⊢ₜ e : TForall τ →
      Γ ⊢ₜ e #() : τ.[τ'/]
-  | TFold e τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜe : TRec τ
-  | TUnfold e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ rec_unfold e : τ.[TRec τ/]
-  | TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ e : TExists τ
-  | TUnpack e1 x e2 Ï„ Ï„2 :
+  | TFold Γ e τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜe : TRec τ
+  | TUnfold Γ e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ rec_unfold e : τ.[TRec τ/]
+  | TPack Γ e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ e : TExists τ
+  | TUnpack Γ e1 x e2 τ τ2 :
       Γ ⊢ₜ e1 : TExists τ →
       <[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
-  | TCmpXchg e1 e2 e3 Ï„ :
+  | 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
+  | TCmpXchg Γ e1 e2 e3 τ :
      EqType τ → UnboxedType τ →
      Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
      Γ ⊢ₜ CmpXchg e1 e2 e3 : TProd τ TBool
-where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
+with val_typed : val → type → Prop :=
+  | Unit_val_typed : ⊢ᵥ #() : TUnit
+  | Nat_val_typed (n : nat) : ⊢ᵥ #n : TNat
+  | Bool_val_typed (b : bool) : ⊢ᵥ #b : TBool
+  | Pair_val_typed v1 v2 Ï„1 Ï„2 :
+      ⊢ᵥ v1 : τ1 →
+      ⊢ᵥ v2 : τ2 →
+      ⊢ᵥ PairV v1 v2 : TProd τ1 τ2
+  | InjL_val_typed v Ï„1 Ï„2 :
+      ⊢ᵥ v : τ1 →
+      ⊢ᵥ InjLV v : TSum τ1 τ2
+  | InjR_val_typed v Ï„1 Ï„2 :
+      ⊢ᵥ v : τ2 →
+      ⊢ᵥ InjRV v : TSum τ1 τ2
+  | Rec_val_typed f x e Ï„1 Ï„2 :
+     <[f:=TArrow τ1 τ2]>(<[x:=τ1]>∅) ⊢ₜ e : τ2 →
+     ⊢ᵥ RecV f x e : TArrow τ1 τ2
+  | TLam_val_typed e Ï„ :
+     ∅ ⊢ₜ e : τ →
+     ⊢ᵥ (Λ: e) : TForall τ
+where "Γ ⊢ₜ e : τ" := (typed Γ e τ)
+and "⊢ᵥ e : τ" := (val_typed e τ).
 
 Lemma binop_nat_typed_safe (op : bin_op) (n1 n2 : Z) Ï„ :
   binop_nat_res_type op = Some τ → is_Some (bin_op_eval op #n1 #n2).