Make array-store/diff a tautology, not a lemma.

There is no reason why the div aux axioms are tautologies, while
the array aux axioms are lemmas.  They are both generated from a
single input clause and easy to interpolate.
Make eq a lemma instead of a tautology

A lemma is something that needs to be interpolated, a tautology is
created from a single source assertion.