fix bug in disequality constraint that made neq only work at the end of a conj
some of the first clause and effect exercises
member and length of list examples from clause and effect (including strange diverging case)
introduce fresh_all(), which should help with the boilerplate a bit