dependent product

the following figure come from coq art, it decribe the 4 possible cases of Prod(s,s',s'') rule
Actually, the first line correspond to simply typed lamda calculus