Proofs of language properties often follow a schema that does not apply just to one language but, rather, applies to many languages of a certain class.

In this paper, we present $\textsc{Lang-n-Prove}$, a domain-specific language for expressing theorems and proofs in such a way that they apply to many languages.
The main characteristic of $\textsc{Lang-n-Prove}$ is that it contains linguistic features that are specific to the domain of language design.

We have used $\textsc{Lang-n-Prove}$ to express the theorems and proofs of canonical forms lemmas, the progress theorem, and the type preservation theorem for a restricted class of functional languages.

We have applied our $\textsc{Lang-n-Prove}$ proofs to several functional languages, including languages with polymorphism, exceptions, recursive types, list operations, and other common types and operators.
Our tool has generated the proof code in Abella that machine-checks the type safety of all these languages, when the correct code for substitution lemmas is provided.