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.