Dramatically reduce encoding times for some equality formulas

[Calvin-L]

Mitigates (but does not entirely fix) #108.

[Calvin-L]

This is definitely an improvement: examples/select-flatmap.ds no longer hangs doing formula encoding. However, now it hangs waiting for Z3. We may need a different approach.