--- a/src/Subset.v	Thu Apr 12 18:46:55 2012 -0400
+++ b/src/Subset.v	Fri Apr 20 12:49:47 2012 -0400
@@ -651,7 +651,7 @@
 Defined.
 (* end thide *)
 
-(** We can build a [sumor] version of the %``%#"#bind#"#%''% notation and use it to write a similarly straightforward version of this function. *)
+(** We can build a [sumor] version of the %``%#"#bind#"#%''% notation and use it to write a similarly straightforward version of this function.  %The operator rendered here as $\longleftarrow$ is noted in the source as a less-than character followed by two hyphens.% *)
 
 (** printing <-- $\longleftarrow$ *)
 
@@ -676,6 +676,8 @@
 Defined.
 (* end thide *)
 
+(** This example demonstrates how judicious selection of notations can hide complexities in the rich types of programs. *)
+
 
 (** * A Type-Checking Example *)