¹⁷Note that if a variable $x$ has a sort $s$ instead of a kind, well sortedness of $\sigma$ means that $\sigma (x)$ must provably have sort $s$ (or lower) according to the equations $E$.