--- a/Paper/document/root.tex	Fri Mar 19 12:31:55 2010 +0100
+++ b/Paper/document/root.tex	Fri Mar 19 15:43:43 2010 +0100
@@ -55,8 +55,8 @@
 very poorly supported with single binders, such as the lambdas in the
 lambda-calculus. Our extension includes novel definitions of
 alpha-equivalence and establishes automatically the reasoning infrastructure for
-alpha-equated terms. This includes strong induction principles that have the
-usual variable convention already built in.
+alpha-equated terms. We can also provide strong induction principles that have 
+the usual variable convention already built in.
 \end{abstract}