This code is heavily inspired by the Dave's talk and it's corresponding implementation in Haskell. Also, have a look on the Dave's STLC tutorial.
Typing relation for the boolean literals is an axiom, so we can infere it:
We are only allowed to get the type of a plain variable from the typing context, no guessing here
If the variable is already annotated with a type, then let us just use this type, not forgeting to check it's consistency