Factor make_tac_under_binders_using_in into two parts

This makes it easier to document.  Also, add more documentation.