Reduce duplication
Merge branch 'master' into functions
Change how inductive counterexamples are sliced