²In formalized type theory, commas and turnstiles can bind even more loosely. For instance, x : A, y : B ⊢c : C is parsed as ((x : A), (y : B)) ⊢(c : C). However, in this book we refrain from such notation until Appendix A.