But if you do step through them, then they do help, whereas a single-tactic proof doesn't tell you what `eta_path_sigma` and `allpath_hprop` get applied to.  (Also, comments help.)

Personally, I think it's unreasonable to be able to expect to understand a tactic script without stepping through it, but I think it is a good goal to write tactic scripts which do help explain the proof to a reader who is stepping through them.