We describe how to formalize syntactical theory abstractly over a choice of concrete syntax using our Coq library Tealeaves. This library provides a monadic interface for datatypes that represent a formal syntax, which is used in lieu of structural recursion on abstract syntax trees. This facilitates a level of modularity and reuse of formal theory that is not readily achieved otherwise, as theory developed with Tealeaves is applicable to the syntax of essentially any formal system. Our interface is specified in terms of a novel class of “structured” monads we call decorated-traversable, which are monads equipped with additional compatible operations. Our talk will discuss the nature of syntactical reasoning, and how Tealeaves fits into this process.