a little more library cleanup

[ecavallo]

• move all the retract stuff to basics.retract (and clean it up a bit)
• minor stuff in paths.s2
• generalize list/set proof to all hlevels