|- (∀l. [] ++ l = l) ∧ ∀l1 l2 h. h::l1 ++ l2 = h::(l1 ++ l2) |- (∀P l1 l2. PART P [] l1 l2 = (l1,l2)) ∧ ∀P h rst l1 l2. PART P (h::rst) l1 l2 = if P h then PART P rst (h::l1) l2 else PART P rst l1 (h::l2) |- ∀P l. PARTITION P l = PART P l [] [] |- (QSORT ord [] = []) ∧ (QSORT ord (h::t) = (let (l1,l2) = PARTITION (λy. ord y h) t in QSORT ord l1 ++ [h] ++ QSORT ord l2))