HoTT/HoTT — pull request #444 by JasonGross (2014-08-29 00:23:25+00:00)
Title: Apply under binders

This tactic will be useful for writing a rewrite modulo associativity
tactic.