Missing (important?) substitution rule I am reading The HoTT Book and I noticed that there is an extensive use of a very reasonable principle: if we have $b \equiv c : A$ then we can conclude $(a =_A b) \equiv (a =_A c) : \mathcal{U}$, for some universe $\mathcal{U}$. "Changing variables" is something we want, so I am perfectly okay with this inference. More generally, the rule should look something like this:
$$
\text{from } B : \mathcal{U} \text{ possibly dependent on $x : A$ and } a \equiv b : A, \text{ derive } B[a/x] \equiv B[b/x],
$$
where $T[t/x]$ denotes the substitution of the term $t$ for $x$ in the expression for the type $T$.
Unfortunately, I could not find or derive a rule of this kind from the formal presentation of type theory in the book (Appendix 2). The closest the book gets is with the substitution rule $\mathsf{Subst}_2$ which postulates a change of the same variable in two definitionally equal types, rather than a change of two definitionally equal variables in the same type. I thought that maybe I could reformulate this in terms of a family of types $B : A \to \mathcal{U}$ (i.e. a family $B : \prod_{x : A} \mathcal{U}$) but there are no rules in the section on dependent products that let me infer $B(a) \equiv B(b)$ from $a \equiv b$.
What am I missing here? Any hint would be appreciated.
 A: The specific rule you mention for equality is one of the congruence rules mentioned (but not displayed explicitly) at the end of section A.2.2: "for all the type formers below, we assume rules stating that each construction preserves definitional equality in each of its arguments".  The general substitution principle is admissible (i.e. provable) based on assuming these primitive rules.  (Thanks Carlo Angiuli for reminding me of this.)  However, it's possible the text would be easier to read if it were more explicit about this.
A: Solved! The answer was in the first subsection (unnumbered) of section A.1, the "informal“ presentation of type theory. Somehow it included stuff that was necessary for A.2, the formal presentation. Anyway, they first define compatibility, denoted by $\downarrow$, between terms $t$ and $t'$ to be a slightly more general equivalence relation than $\equiv$ that takes $\lambda$-abstraction into account. In particular, the first rule states that from $t \downarrow t'$ and $s \downarrow s'$ one can derive $t(s) \downarrow t'(s')$. They also define $t \equiv t' : A$ as the combined judgment $t : A, t' : A, t \downarrow t'$. So, since $B \downarrow B$ for $B : A \to \mathcal{U}$, when $a \equiv b : A$ we can derive $B(a) \downarrow B(b)$, and since $B(a), B(b) : A$ we conclude that $B(a) \equiv B(b)$.
