--- a/src/InductiveTypes.v	Mon Nov 09 11:48:27 2009 -0500
+++ b/src/InductiveTypes.v	Mon Nov 09 13:18:46 2009 -0500
@@ -437,7 +437,7 @@
 Implicit Arguments Nil [T].
 (* end hide *)
 
-(** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. *)
+(** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed.  We verify that this has happened using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)
 
 Print list.
 (** %\vspace{-.15in}% [[