Prove triples by symbolic evaluation

[serras]

Note for reviewers: I've kept the previous implementation of incorrectnessPaths as it was, and worked in a new module Symbolic.Prove. The main difference is that the new implementation uses terms as input, instead of constraints.

In general, the idea of the implementation is to symbolically evaluate the function, the assumption, and the thing-to-be-proven in parallel (we can devise better ways to handle this later). At every step -- which may have turned into several independent branches due to the magic of SymEvalT -- we check whether:

   result == current term for function
&& translation of current term for assumption
=> translation of current term for thing-to-be-proven

In any of those return Sat and we are done with translation, that means we've found a counterexample. If it's Unsat, the branch can be pruned. In any other case we just keep exploring.

[serras]

This is ready for review. I've just pushed a final change which pushes down type information given the constructor. For example, if we have a tuple and we know the type is (Int, Bool), when translating each component we push the respective type down.