HoTT/HoTT — pull request #451 by JasonGross (2014-09-01 18:16:25+00:00)
Title: Transitivity

Now that tactics like `symmetry` are defined in Coq-land in the stdlib, thanks to Pierre-Marie Pédrot, we can define our own versions that, after unfolding, result in proofs using things like `concat`. I've replaced `apply symmetry` with `symmetry` and `path_via` with `transitivity` (appending `auto with path_hints` to the cases that need it). I've removed the `path_via` tactic. If we want to keep `path_via`, I can strip the commit that removes `path_via` and inserts explicit `auto with path_hints`.

A question: Do we want to mark the relevant constants as auto-unfolding, so that when we `simpl`, proofs built will `transitivity` and `symmetry` will unfold to uses of `concat` and `inverse`?