Add another example to 5.2

This one is a bit less robust in the face of CoqMT, but has the functions
satisfying the same recurrence judgmentally.
Merge pull request #325 from JasonGross/ex-5-2

Add another example to 5.2