RFC: disjunction of guard conditions for grind_pattern

[pirapira]

I propose extending grind_pattern so that it can take conjunctive normal form (conjunction of disjunctions) of side-conditions. Currently grind_pattern can take a list of side-conditions. The list is interpreted as a conjunction.

The motivating example for the change is mod_eq_of_lt: a < b -> a % b = a. It's desirable to guard against using this lemma on completely concrete examples like 2 % 1024. However, both 2 % b and a % 1024 can benefit from the lemma.

To distinguish the wanted case and unwanted case, the precise guard would look like

grind_pattern mod_eq_of_lt => a % b where
  guard a < b
  not_value a || not_value b

with disjunction ||.