correct unit elimination rule

The unit elimination rule had a spurious additional bound variable that has been removed.
notation for left- and right-whiskering

it seems preferable to use a sans-serif subscript to indicate left- and right-whiskering.  prior to this change the subscripts used in the eckmann-hilton proof conflict with the use of l and r as variables.
(Marked) errata for the correction of the unit elimination rule.