  We introduce a universe of regular datatypes with variable binding
information, for which we define generic formation and elimination (i.e.
induction /recursion) operators. We then define a generic alpha-equivalence
relation over the types of the universe based on name-swapping, and derive
iteration and induction principles which work modulo alpha-conversion capturing
Barendregt's Variable Convention. We instantiate the resulting framework so as
to obtain the Lambda Calculus and System F, for which we derive substitution
operations and substitution lemmas for alpha-conversion and substitution
composition. The whole work is carried out in Constructive Type Theory and
machine-checked by the system Agda.
