Add sequence method via reflect.internal.Sequenceable implicit
And, Or take sets of Props

Remove redundant UniqueSym class.
Don't eagerly CNF transform when removing equality.

Simplify resulting proposition before solving.
SI-6582 Use Tseitin's algorithm for CNF.

This resolves the `AnalysisBudgetException` problem for big pattern matches.

Initial experiments indicate that the problem is even simpler than initially
thought: all formulae I got from the exhaustiveness check could be transformed
directly into CNF. Thus the framework introduced here might be overkill
and a much simpler implementation could work as well.

For Scala 2.11 I'd suggest to replace the DPLL procedure with Sat4j.