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