+<!--
+I would like to propose one pedegogical suggestion (due to Ken), which
+is to separate peg addition from non-determinacy by explicitly adding
+a "Let" construction to GSV's logic, i.e., "Let of var * term *
+clause", whose interpretation adds a peg, assigns var to it, sets the
+value to the value computed by term, and evaluates the clause with the
+new peg in place. This can be added easily, especially since you have
+supplied a procedure that handles the main essence of the
+construction. Once the Let is in place, adding the existential is
+purely dealing with nondeterminism.
+-->
+