select ITP-TOOL .
loop init-itp .

(goal ins1 : INSERT-SORT-VERIFICATION 
      |- A{L:List}((sorted(sort(L:List))) = (true)) .)