HoTT/HoTT — pull request #166 by JasonGross (2013-08-06 01:47:36+00:00)
Title: Improve the [symmetry] and [etransitivity] tactics

It seems that [apply] uses an inferior(?) unificiation engine. That of
[refine] and [exact] (and even [eapply], in some cases) are better, in
my experience.