Metatheory is concerned with proving properties about theories, in this case type theories or programming languages.