HoTT/HoTT — pull request #147 by jcmckeown (2013-07-10 02:18:26+00:00)
Title: Redundancy never hurt, right?

Variation on dpath_forall; found it handy for generalizing Flattening lemmata.