# Tag Info

Perhaps what you're missing (although you seem to suspect) is that the left hand side of the $⊢$ is not just for specifying what types variables have. In fact, as you've noted, it doesn't necessarily have all (or only) the variables on the right hand side (although in this situation it does only have variables, not things like $λy.x : α→β$). What it's doing ...