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].
implicit arguments in quotient.v, close #447
make setrel notation global is_mere_relation in Overture
remove unnecessary Let in Quotient module
oops
coqdoc
unify ap_ap10 and apD10_ap_*
Merge pull request #450 from mikeshulman/quotient

implicit arguments in quotient.v, close #447
Merge pull request #452 from JasonGross/remove-useless-match

Remove a useless match
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]"
Restore the old definition of path_via

As per #454 / #451.
Merge pull request #455 from JasonGross/restore-path-via

Restore the old definition of path_via
Work around bug 3545

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3545, certain [apply]s
fail (with "No applicable tactic") when they should not
Work around bug 3563

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3563, Anomaly:
Uncaught exception Not_found(_). Please report. on pattern matching on
an eta-expanded primitive projection
Work around bug 3559

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3559, Trouble unifying
universes across fixpoints (cannot unify "(fix foo : Type@{U} := bar) a
b" with "(fix foo : Type@{V} := bar) a b")