diff -r 4355eb3b7161 -r 572064152e8a Paper/document/root.tex
--- a/Paper/document/root.tex	Fri Mar 19 18:42:57 2010 +0100
+++ b/Paper/document/root.tex	Fri Mar 19 18:43:29 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}