ESPL: Fix typing lemmas for automation
ESPL: Combine (non-)match step constructors

We keep a single constructor for pattern matching and inequality constraints,
distinguishing them by a boolean flag. The message to be matched by a pattern
must be a single variable.
Also clean up.