remove unneeded ghost commands
add proof for take_plus_one
add some todos/fixes