Substitution of expressions for free variables in terms is one of the most basic operations in mathematical practice. As soon as bound variables are present, those variables must not capture free variables of the same name that may have occurred in the expressions that become subexpressions of the result. In pure lambda-calculus, this problem is studied in isolation. Of course, there are already satisfying answers that also allow a formalization on computers. One of them is by using families of inductive datatypes, i. e., a parameterized generation process of lambda-terms, with the set of allowed names of free variables as the parameter. Proving that such a representation respects the basic properties of substitution dictated by category theory is not trivial and quite recent work, e. g., on the Coq theorem
proving environment.

There are more nice examples of the use of inductive families, e. g., a redecoration algorithm for finite triangular matrices that is very succinct in comparison with list-based representations (and whose soundness proof has only recently been found based on the most recent extension to the Coq system).

We want to go one step further: We want to be able to encapsulate some subexpressions as if they were just variable names. This yields lambda-calculus with "explicit flattening" whose representation by inductive families needs induction principles that are not offered by
any theorem proving environment, but that could be encoded within Coq. Here, already the notion of a free occurrence of a variable will challenge mathematical minds.

Fortunately, the whole verification of the basic substitution properties could be carried out within Coq, whence we can just concentrate on discussing which generation principles are needed and in which way they are more difficult than plain mathematical induction
over the natural numbers.