Define custom [transitivity] and [symmetry].

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].
Remove many [path_via] and [apply symmetry]

Now [symmetry] and [transitivity] work.  Should we remove remaining uses
of [path_via], and replace it with its body, [transitivity foo; auto
with path_hints]?
Remove [path_via]

Replace remaining uses of [path_via mid] with [transitivity mid; auto
with path_hints].
unify ap_ap10 and apD10_ap_*
Merge pull request #451 from JasonGross/transitivity

Transitivity
Merge pull request #449 from mikeshulman/ap10ap

unify ap_ap10 and apD10_ap_*
Revert "Remove [path_via]"

This reverts commit dd9121da211cdcb3cdb434a0da2cf10b178eee58.

As per @mikeshulman's
https://github.com/HoTT/HoTT/pull/451#issuecomment-54104523:

> I don't understand why we are so cavalier about replacing a tactic
> that's used throughout the library by a tactic that does something
> different.  I think we should revert this change and then continue the
> discussion about the advantages and disadvantages of all possible
> options before making a decision.

> My experience suggests that even if we manage to make transitivity
> "pretend" that it is just concat, eventually it will bite someone
> somewhere.

> Also, there's undoubtedly a reason why we added `auto with path_hints`
> to `path_via`.  Is the questionable advantage of calling the tactic
> "transitivity" worth having to type that manually every time we need
> it?
Merge pull request #453 from JasonGross/revert-remove-path-via

Revert "Remove [path_via]"