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.