From: acondolu <andrea.condoluci@unibo.it>
Date: Fri, 27 Jul 2018 17:36:55 +0000 (+0200)
Subject: More comments and small fixes
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0fd76d8a70c67669bae7798495d33dad55bc3c6f;p=fireball-separation.git

More comments and small fixes
---

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