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".