Interesting. Are there more examples somewhere? I'm curious about cases where multiple examples are required. The associativity "example" corresponds directly to the rewrite rule definition, so it doesn't really illuminate the distinction between specifying a rewrite rule and inferring a rule from multiple examples.
Right, associativity is the simplest case because the structure is visible
directly in one example.
The system needs multiple examples when there is more than one varying part
and a single example is ambiguous. A simple example is wrapping a function
call. With: