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.