Modal logics have numerous applications in computational linguistics, artificial intelligence, rule-based reasoning, and, in general, alethic, deontic and epistemic contexts. Higher-order quantified modal logics additionally incorporate the expressiveness of higher-order formalisms and thereby provide a quite general reasoning framework. By exploiting this expressiveness, the Modal Embedding Tool (MET) allows to automatically encode higher-order modal logic problems into equivalent problems of classical logic, enabling the use of a broad variety of established reasoning tools. In this system description, the functionality and usage of MET as well as a suitable input syntax for flexible reasoning with modalities are presented.