include first version of Bits2Integer
use Bits2Integer in contract of peek
use Bits2Integer in loop invariant of peek