making the lexer more obviously total
cheating a slow auto proof, needs fix
finished init code proof