HoTT/HoTT — pull request #625 by JasonGross (2014-11-24 23:12:37+00:00)
Title: .+3, .+4, .+5

I figured I'd stop at a common number like 5. I can go back and remove .+4 and .+5 (because they're currently unused), or I can go up to some other number instead, if that's preferred.