Simplified the quicksort example so that the permutation predicate
isn't proven with props. Instead, I want to move it to the SMT solver
like I did with insertion sort.