On page 195 of Pierce's TAPL book, he states that one can replace a down-cast operator by some sort of dynamic type test. Then he gives the following figure:

There is no further explanation and I'm unaware of how to interpret these rules. Why $\Gamma$ is missing from the second and third? Where does $x$ or $t_i$ come from? What does it mean $in$?...