Well-founded recursion is a technique to turn recursion which decreases along a well-founded ordering into a structural recursion.