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