fact: Parameter quicksort_equation : forall l : list A, quicksort l = match l with | nil => nil (A:=A) | h :: tl => let (l1, l2) := partition h tl in quicksort l1 ++ h :: quicksort l2 end.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)