HoTT/HoTT — pull request #313 by JasonGross (2014-02-05 20:40:54+00:00)
Title: Make the inverse of functor_forall transparent

If being able to step through the proofs in proviola is preferred, I can instead stuff this in a section and make separate lemmas for the proofs.