A formalization of a bidirectional typechecker for STLC with booleans