  We implement three Coq plugins regarding inductive types in MetaCoq. The
first plugin is a simple syntax transformation generating alternative
constructors for inductive types by abstracting over concrete indices in the
types of the constructors. The second plugin re-implements Coq's
$\texttt{Scheme Induction}$ command in MetaCoq, and extends it to nested
inductive types, e.g. types like rose trees which use $\texttt{list}$ in their
definition, similar to the Elpi-plugin by Tassi. The third plugin implements
the $\texttt{Derive Subterm}$ command provided by the Equations package in
MetaCoq.
