provide directory for future driver
admit two helper lemmas (for the time being)
remove generation of *.i files
add new helper function
reimplement with PeekBit64
use old function