formatting
simplify proof of Bitwalker_Peek
remove old proofs
remove more old proofs
simply verification of PokeThenPeek