Induction on typing derivation in refinement types system
It's a form of structural induction. 

As we see on page 12 of the text, the typing relation is defined inductively by four rules. 

For example, the rule abs says that given a deduction $\Gamma, x:r \vdash t : S$ we can form the new deduction $\Gamma \vdash \lambda x.t : R \to S$. 

Compare with how, given a natural number $n$ you can form a new natural number $n+1$.

To prove a proposition $P(n)$ about an arbitrary natural number by induction you note that $n$ is either 


$0$, or
$m+1$ for some $m$ 


In the first case, you prove $P(0)$ directly. In the second, you assume you have a proof of $P(m)$ and use this to prove $P(m+1)$.

Similarly, to prove a proposition about an arbitrary derivation $\Delta$ of the type judgement $\Pi \vdash t :R$ you note that $\Delta$ is either


$ \dfrac{}{\Pi \vdash x : R}\textsf{ var}$ and $t=x$ a variable
$\dfrac{\Pi \vdash s : S \to R, \Pi \vdash u : S }{\Pi \vdash s(u) : R}\textsf{ app}$ and $t=s(u)$, an application, for some derivations $\Delta_1, \Delta_2$ of the type judgements $\Pi \vdash s : S \to R, \Pi \vdash u : S $
$\dfrac{\Pi, x:r \vdash s : S}{\Pi \vdash \lambda x.s : R \to S}\textsf{ abs}$ and $t=\lambda x.s$, an abstraction, for some derivation $\Delta_1$ of the type judgement $\Pi \vdash s : S$
$\dfrac{\Pi \vdash t:S, R \leq R}{\Pi \vdash t : R}\textsf{ sub}$, for some supertype $S$ of $R$ and a derivation $\Delta_1$ of $\Pi \vdash t : S$


In the first case, you prove $P(\Delta)$ directly, and in the other three you assume $P(\Delta_1)$ and $P(\Delta_2)$ and then prove $P(\Delta)$.

There is an example in the proof of lemma 2.3.10 of the text, page 33.