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 : X<:T11. T12    ,    ctx |- T2<:T11   -----------------------------------------------            ctx |- t1 [T2] : [X-->T2]T12I 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 
System f-sub, how to do type checking?
type theory;type checking;type inference
It would've helped if you mentioned what page that rule appears in.Anyhow, from what I can tell here's an example. t :  X <: Animal. X makes noise             Cat <: Animal------------------------------------------------------------                       t [Cat] : Cat makes noiseThe idea seems to be that t is to be treated as a generic function, or a dependently-typed function, in that for each Animal subtype X, in our example, it gives us a proof t[X] and the rule just formalises this idea.Hope that helps.