Datatype-generic programming can be used for language formalisation. Inductive types in dependently typed languages can express highly complex inductive definitions, including the formalisation of programming languages. By applying the idea of datatype-generic programming to this setting, we can establish results uniformly for classes of languages rather than treating each language in isolation. In this talk, using Agda as the host language, we will discuss what can be achieved generically for languages beyond substitution lemmas, and identify what remains open—both in theory and in practice—for more expressive languages.