add Bitwalker_Peek_Core and adapt proofs
remove old proofs
remove assertion
add Bitwalker_Poke_Core and adapt proof
format and rename labels for Bitwalker_Poke
minor