--- a/LMCS-Paper/Paper.thy	Thu Sep 08 13:03:19 2011 +0100
+++ b/LMCS-Paper/Paper.thy	Fri Sep 09 11:52:24 2011 +0100
@@ -359,7 +359,7 @@
   infrastructure for alpha-equated terms.\smallskip
 
   The examples we have in mind where our reasoning infrastructure will be
-  helpful includes the term language of Core-Haskell (see
+  helpful include the term language of Core-Haskell (see
   Figure~\ref{corehas}). This term language involves patterns that have lists
   of type-, coercion- and term-variables, all of which are bound in @{text
   "\<CASE>"}-expressions. In these patterns we do not know in advance how many
@@ -571,7 +571,7 @@
   
   \begin{equation}\label{equivariance}
   @{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;
-  @{text "\<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
+  @{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
   \end{equation}\smallskip
    
   \noindent