Some points about type checking of simply typed $\lambda$-calculus? type checking

I was preparing examples of type checking in simply typed $\lambda$-calculus. I wanted to explain it to my audience in the way of implementation. And I found a bit tricky point in the typing rule of application, which is as follows.

$$
   \frac  {\Gamma \vdash t_1:T_{11}\rightarrow T_{12} \quad \Gamma \vdash t_2:T_{11}}
   {\Gamma \vdash t_1 \, t_2 :T_{12} }
 $$

$$
   \frac  {\Gamma, x:T_1 \vdash t_2 :T_2}
   {\Gamma \vdash \lambda x:T_1.t_2 : T_1 \rightarrow T_2}
 $$

Typing rules for booleans are:

$$
   \frac  {}
   {\Gamma \vdash \texttt{true}: bool }
 $$

$$
   \frac  {}
   {\Gamma \vdash \texttt{false}: bool }
 $$

My question

As far as I know, we do not need unification for type checking in the typed $\lambda$-calculus, we need unification in type inference. However, the following type checking example seems that we need something like unification, also it seems that type checking is leading to type construction. 

$$
   \frac  { \vdash \lambda x:bool.x: T \rightarrow bool  \quad \vdash \text{true}: T}
   { \vdash (\lambda x:bool.x) \text{ true}: bool }
 $$
Here, $T$ is unknown type variable. It is easy to saying that $T$ is $bool$ because of the boolean typing rules, so we can continue the left branch of the above type checking as follows.

$$
\frac {x:bool \vdash x:bool}
{ \vdash \lambda x:bool.x: bool \rightarrow bool }
$$

The premise is true, so the type checking is successful.

But how do we know the value of $T$ in an implementation?
It should take matching $ true:bool$ to $true: \text{T}$ to know $T$ is $bool$. But this seems unification to me.

Also, finding $T$ for $\Gamma \vdash t: T$ is a type inference problem. So, the above type checking is leading to type inference. Am I correct?  

Does type checking of the simply typed $\lambda$-calculus need unification?

Does type inference appear when doing type checking?

Please correct me if I am wrong at any point and explain.

Other info

Type checking of ${ \vdash (\lambda x:bool.x) \text{ true}: bool }$ is given as an example in the book "types and programming languages", page 103. However, it did not specify how $T$ is obtained.
Its derivation concluded $T$ is $bool$ when using the typing rule of application, as shown below.

$$
   \frac  { \vdash \lambda x:bool.x: bool \rightarrow bool  \quad \vdash \text{true}: bool}
   { \vdash (\lambda x:bool.x) \text{ true}: bool }
 $$

I believe these details are ignored in the book.
Your example is poorly chosen. In $(\lambda x : \mathsf{bool} . x) \, \mathsf{true}$ you can obviously read off the type from the $\lambda$-abstraction because it tells you that $x$ should have type $\mathsf{bool}$. A more relevant example is
$$
((\lambda f : \mathsf{bool} \to \mathsf{bool} . f) (\lambda x : \mathsf{bool} . x)) \, \mathsf{true} : \mathsf{bool}
$$
Now we are faced with determining $T$ by looking at $(\lambda f : \mathsf{bool} \to \mathsf{bool} . f) (\lambda x : \mathsf{bool} . x)$.

The usual algorithm to be used for this sort of thing is bidirectional typechecking: some terms have their types checked but others have their types inferred. No unification is required, because all types are inferred immediately. (Unification happens when we postpone decisions until a later time.)