Making solve_sorted more robust - no longer dependent on Opaque List.app.
Add pstacs.v (proof search tactics).  Simplify some proofs in sets.v.
Update todo.  Try to get around github insisting on (incorrectly)
renumbering bullets at top of readme.