diff --git a/coq/lemmas/subst_lemmas.v b/coq/lemmas/subst_lemmas.v
index 7c5634c..e6e994e 100644
--- a/coq/lemmas/subst_lemmas.v
+++ b/coq/lemmas/subst_lemmas.v
@@ -247,6 +247,13 @@ Proof.
     discriminate.
     apply eq_sym, H1.
     assumption.
+
+  - unfold expr_open in *.
+    pick fresh x for L.
+    apply expr_open_lc_core with (i:=0) (s1:=(ex_fvar x)) (j:=S k) (s2:=s).
+    discriminate.
+    apply eq_sym, H1.
+    assumption.
 Qed.
 
 (*
diff --git a/coq/terms/debruijn.v b/coq/terms/debruijn.v
index 1c78ef0..f6e0505 100644
--- a/coq/terms/debruijn.v
+++ b/coq/terms/debruijn.v
@@ -242,7 +242,7 @@ Fixpoint expr_open_rec (k:nat) (t:expr_DeBruijn) (e:expr_DeBruijn) {struct e} :
     | ex_morph σ e' => ex_morph σ (expr_open_rec (S k) t e')
     | ex_abs σ e' => ex_abs σ (expr_open_rec (S k) t e')
     | ex_app e1 e2 => ex_app (expr_open_rec k t e1) (expr_open_rec k t e2)
-    | ex_let e1 e2 => ex_let (expr_open_rec k t e1) (expr_open_rec k t e2)
+    | ex_let e1 e2 => ex_let (expr_open_rec k t e1) (expr_open_rec (S k) t e2)
     | ex_ascend σ e' => ex_ascend σ (expr_open_rec k t e')
     | ex_descend σ e' => ex_descend σ (expr_open_rec k t e')
   end.
@@ -285,7 +285,10 @@ Inductive expr_lc : expr_DeBruijn -> Prop :=
       (forall x, (x `notin` L) -> expr_lc (expr_open (ex_fvar x) e1)) ->
       expr_lc (ex_morph σ e1)
   | Elc_App : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_app e1 e2)
-  | Elc_Let : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_let e1 e2)
+  | Elc_Let : forall e t L,
+      expr_lc e ->
+      (forall x, (x `notin` L) -> expr_lc (expr_open (ex_fvar x) t)) ->
+      expr_lc (ex_let e t)
   | Elc_Ascend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_ascend τ e)
   | Elc_Descend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_descend τ e)
 .