diff --git a/semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex b/semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex
index f46a3e8..928dd44 100644
--- a/semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex
+++ b/semester4/fmfp/parts/02_typing/01_mini-haskell/01_lambda-calculus.tex
@@ -19,3 +19,5 @@ It is based on the same concept as natural deduction trees
         \infer2[App]{\Gamma \vdash (t_1 t_2) :: \tau}
     \end{prooftree}
 \]
+
+For rule \texttt{Abs}, we require that $x \notin \Gamma$