select ITP-TOOL .
loop init-itp .

(goal ins2 : INSERT-SORT-VERIFICATION |- A{L:List}
    ((mset(sort(L:List))) = (mset(L:List))) .)