To enforce termination, Rocq requires that non-structurally recursive functions use well-founded recursion, which is supported by plugins such as Equations. Alternatively, we can explicitly perform structural recursion on an auxiliary accessibility argument, as proposed by Leroy (2024). This paper systemizes Leroy’s method, proposing a design pattern that supports function definition by well-founded recursion as well as proofs by induction over the well-founded relation.