Structural normalization algorithm for the simply typed lambda calculus
You can: define /hereditary substitution/ on already normalized STLC terms using structural induction (where the induction is (in part) on the type).
I couldn't find the reference I was thinking of right now, but a quick search for &quot;agda hereditary subtitutions STLC&quot; pointed to various relevant pages, such as https://github.com/ezyang/lr-agda/blob/master/STLC.agda