bufixes and the bugs

bufixes and the bugs

* array now only propagates thropugh the equality engine
* assertions in the equality rewriting to ensure eq -> { eq, T, F }