stlc Bidirectional Simply-Typed Lambda-Calculus with Booleans, with type annotations required for abstractions