Add comments to make_tac_under_binders_using_in

As per https://github.com/HoTT/HoTT/issues/536#issuecomment-57209389.
Factor make_tac_under_binders_using_in into two parts

This makes it easier to document.  Also, add more documentation.
Add another line of documentation
Merge pull request #540 from JasonGross/comment-make_tac_under_binders_using_in

Add comments to make_tac_under_binders_using_in