remove property valid_result
save state
adapt proof to UpperBitsNotSet
verify auxilliary function UpperBitsNotSet64
adapt proof of property copied
move UpperBitsNotSet64 to Bit64
adapt contract and proofs of PokeThenPeek
adapt contract and proof of Bitstream_Write