reorder intro Bit64
remove substitutions in proofs of Bitwalker_Peek
remove substitutions in proof of Bitwalker_Poke