Proof production for arrays.  This needs more testing, but should in general be okay.  This commit essentially fixes the meaning of the new proof element :weakpath to be a path through the weak equivalence (modulo i) graph.  It is a path in the modulo graph if there are two selects on that path.
Fixed treatment of @diff.  The axiom for @diff was wrong and included multiple times in the clause database.