Fix equivication between variables in expressions and rules

[bemica]

Because the variables used in rules are considered completely separate than the variables used in expressions, there is some unexpected behavior.

e.g. If the rule is p≡q, the user probably intends to substitute p in the left hand expression with q in the right hand expression. However, this rule actually means "any expression is equivalent to any other expression" and will always validate on any two expressions

[NicMcPhee]

I'm not really sure what your intent here is. Do you think we should have a syntax that allows us to essentially define constants (e.g., x = 4 that allows us to replace x with 4)?

[bemica]

I think that would be good. The syntax with variables seems just very unintuitive to me, because a variable x in expressions has no relation to a variable x in the rule. But maybe it would be sufficient to just add some warning if the user uses the same variable name in expressions and rules