Add simplification instance for list ≠ [], needed for quicksort

When doing the quicksort exercise, RefinedC would at some point get stuck on a goal of the form some_list ≠ [] ∧ …, where some_list is a protected evar. This merge request adds an instance simplifying l ≠ [] into ∃ a l', l = a :: l' whenever l is a protected evar.

Additionally, it adds the sorting function to tutorial/quicksort_solution.c for which this instance was necessary.