HoTT/HoTT — pull request #540 by JasonGross (2014-09-29 19:11:29+00:00)
Title: Add comments to make_tac_under_binders_using_in

As per https://github.com/HoTT/HoTT/issues/536#issuecomment-57209389.