More comments and small fixes

diff --git a/notes.tex b/notes.tex
index 264e827a00f9dda3ab29415e7654e6a6a5778b5d..c4e4cfdfa015e5296236c1ca136055b46a685691 100644 (file)
--- a/notes.tex
+++ b/notes.tex
@@ -380,7 +380,7 @@
   $\nf{\tm\sigma}\EtaNeq\nf{\tmtwo\sigma}$.\r
   Let $\tm \EtaEq \lambda\vec\vartwo.\, h_1\,\vec a$ and \r
   $\tmtwo \EtaEq \lambda\vec\vartwo.\, h_2\,\vec b$,\r
-  with $|\vec\vartwo| = \xK$.\r
+  with $|\vec\vartwo| = \xK$ {\color{red}[Capire perche' si puo' $\xK$-$\eta$-espandere qui]}.\r
   By (course-of-value) induction on the size of $\tm$ and $\tmtwo$,\r
   and by cases on the definition of eta-difference:\r
   \begin{itemize}\r
@@ -401,9 +401,10 @@
      \r
      We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
      \begin{itemize}\r
-       \item Both $|\vec a|,|\vec b|\leq i$: \TODO\r
-       \item w.l.o.g. $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO\r
-       \item Both $|\vec a|,|\vec b|> i$: \TODO use the lemma above\r
+       \item $|\vec a|,|\vec b|\leq i$: \TODO\r
+       \item $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO\r
+       \item $|\vec a|\leq i$ and $|\vec b|> i$: symmetric to the case above.\r
+       \item $|\vec a|,|\vec b|> i$: \TODO use the lemma above\r
        plus another one. Reason on the numebr of arguments\r
        $\Args{\nf{a_i\sigma\vec\alpha}}$ vs  \r
        $\Args{\nf{b_i\sigma\vec\alpha}}$.\r
@@ -417,7 +418,7 @@
     \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
     and we conclude by \ih{} since $a_n \EtaNeq b_n$ implies that \r
     $\nf{a_n\sigma} \EtaNeq \nf{b_n\sigma}$.\r
-    {\color{red}[Can we use the \ih{} here?]}\r
+    {\color{red}[Capire se possiamo davvero usare l'\ih{} qui]}\r
     \r
     We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
     \begin{itemize}\r