Insertion sort in lists

fully automatic with help of CVC3

does not work without permut in insert post-cond

permut could be weakened to subset ?

module InsertionSortList

  use import int.Int
  use import list.List
  use import list.Mem
  use import list.SortedInt
  use import list.Permut

let rec insert x l
    requires { sorted l }
    ensures { sorted result /\ permut result (Cons x l) }
 =  match l with
    | Nil -> Cons x Nil
    | Cons y l' -> if x <= y then Cons x l else Cons y (insert x l')
    end

let rec insertionSort l
    ensures {sorted result}
 =  match l with
    | Nil -> Nil
    | Cons x l' -> insert x (insertionSort l')
    end

end