Add support for ; (or) in rules

[bvssvni]

Currently, the only logical connectivity supported is , (and).

The way the inference rule should work, is that variables are bound and substituted as usual, but branches with OR reduces when any sub-expression is constant.

[bvssvni]

One idea is to support it in left-side expressions.

(a, b); (b, a) :- (a, prod), (b, prod).

Alternatively, this could be using commas:

(a, b), (b, a) :- (a, prod), (b, prod).