diff --git a/theories/logrel/ltyping.v b/theories/logrel/ltyping.v
index e02da57d2e18c9ea9c9a5fa044f22ed6bdd086d2..e92639540fbbc9e25166df1c7419c8bf4ea78a1d 100755
--- a/theories/logrel/ltyping.v
+++ b/theories/logrel/ltyping.v
@@ -64,6 +64,9 @@ Section Environment.
              (vs : gmap string val) : iProp Σ :=
     ([∗ map] i ↦ A ∈ Γ, ∃ v, ⌜vs !! i = Some v⌝ ∗ lty_car A v)%I.
 
+  Lemma env_ltyped_empty vs : ⊢ env_ltyped ∅ vs.
+  Proof. by iApply big_sepM_empty. Qed.
+
   Lemma env_ltyped_lookup Γ vs x A :
     Γ !! x = Some A →
     env_ltyped Γ vs -∗ ∃ v, ⌜ vs !! x = Some v ⌝ ∗ A v ∗ env_ltyped (delete x Γ) vs.
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index 5e55d180bdf8f2ed1baa796689edafd38bea1a00..8d7d4413ad69ab818f40bef9ed41e24474374286 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -190,17 +190,20 @@ Section properties.
     iApply wp_frame_r. iFrame "HΓ". iApply ("Hf" $! v with "HA1").
   Qed.
 
-  Lemma ltyped_lam Γ Γ2 x e A1 A2 :
-    (binder_insert x A1 Γ ⊨ e : A2 ⫤ Γ2) -∗
-    Γ ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ binder_delete x Γ2.
+  Lemma ltyped_lam Γ Γ1 Γ2 Γ3 x e A1 A2 :
+    env_split Γ Γ1 Γ2 -∗
+    (<[ x := A1 ]>Γ2 ⊨ e : A2 ⫤ Γ3) -∗
+    Γ ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ Γ1.
   Proof.
-    iIntros "#He" (vs) "!> HΓ /=".
-    wp_pures.
-    (* Unprovable *)
+    iIntros "#Hsplit #He" (vs) "!> HΓ /=".
+    iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
+    iFrame "HΓ1". wp_pures.
     iIntros (v) "HA1". wp_pures.
-    iDestruct ("He" $!((binder_insert x v vs)) with "[HΓ HA1]") as "He'".
-    { iApply (env_ltyped_insert with "[HA1 //] [HΓ //]"). }
-    destruct x as [|x]; rewrite /= -?subst_map_insert //.
+    iDestruct ("He" $!((binder_insert x v vs)) with "[HA1 HΓ2]") as "He'".
+    { iApply (env_ltyped_insert with "[HA1 //] HΓ2"). }
+    rewrite -subst_map_binder_insert.
+    iApply (wp_wand with "He'").
+    iIntros (w) "[$ _]".
   Qed.
 
   Lemma ltyped_let Γ Γ1 Γ2 (x : binder) e1 e2 A1 A2 :