I've started reading the HoTT book and am trying to understand its formal treatment of Martin-Löf type theory. Something small in the "first presentation" of the appendix has tripped me up; see the screenshot attached below for reference. In particular, the last two "alternative style" rules are not entirely clear to me. For one, surely the second should read "if $x:A\vdash b:B(x)$ then $\lambda x.b:\Pi_{(x:A)}B(x)$"? This seems to me a rather important point as $B$ and $B(x)$ are distinct terms. For the other, surely the third holds only if $x$ does not occur free in $B$? This may be implicit but it seems unclear to me.
