Defunctionalization, a process to transform higher-order programs into first-order ones, has been heavily studied for its structure, its use-cases, its logical semantics, etc. This extended abstract is an invitation to study defunctionalization through the prism of a shallow embedding in an interactive theorem prover. We use metaprogramming techniques to automatize program transformation and proof generation, with a starting implementation in Rocq. The long term goals are to define defunctionalization for a large subset of Type Theory, to prove and generate proofs such as semantics and termination preservation, and more generally to use metaprogramming with strong guaranties to have a better understanding of this program transformation.