Good catch! Forgot to mention it. Yeah, Chlipala certainly practices what he preaches by building lots of useful tools for the rest of us using the very methods he writes about. Moreover, tools that catch or prevent lots of problems in other useful apps or tools. The kind of researcher and research we can always use more of. :)