System f-sub, how to do type checking?

I was reading that system f-sub (polymorphic lambda calculus with sub-typing) and I was quite confused with its one checking rule called "T-TAPP".

This rule as following (ctx denotes the typing context)

ctx |- t1 : ∀XT2]T12

I could not understand how '[x-->T2]T12' will be used (I know it is substitution). This rule appears on page 10 in the following source.
I am looking for two type checking examples, in which above inference rule will be applied and at least one example is a case of type checking failure.

Could anyone provide me with concrete examples?

Description of system F-sub

I know this is old but the previous answer has a huge misconception.

The following function is in System F.

$f = \lambda X. X \rightarrow X \rightarrow X$

All we know of this function is it selects one of its arguments and can be instantieded with any type; $\ f$ [Bool] : Bool $\rightarrow$ Bool $\rightarrow$ Bool.

In System $F_{<:}$ is possible to have the following function.

$f' = \lambda X<:$Number$.\ X \rightarrow X \rightarrow X$

This function can be the addition, multiplication, division, subtraction, etc, and can be instantiated with subtypes of Number.

$f'$ [Int], $\ f'$ [Double], $\ f'$ [Real] are valid instantiations, but $\ f'$ [Bool] not, because Bool is not a subtype of Nat.

Dependent types are a different thing. It has nothing to do here and is out of the scope of the question, but it is a very interesting topic. See Lambda Cube

StackExchange Computer Science Q#59981, answer score: 3