Work on array pf signature, add working example.  Add quantifiers proof signature. Ignore terms not in current master EE for QCF.  Minor refactoring.  Make --rewrite-rules true by default.