I made a mistake in my previous message. The LHS is the "when" part of the
rule.
Also, it appears you may have misunderstood the syntax of the LHS where something like X(
z == y )
is not a call to a function, but a question of fact to be interpreted as "there is an
instance of
class X with field z equal to the value y".