HoTT/HoTT — pull request #325 by JasonGross (2014-02-26 17:32:37+00:00)
Title: 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.