TypeClasses for Refl, Sym, Trans applied to Paths and Equiv.

The tactic "symmetry" was not working.  We figured the better long term solution was to use a TypeClass for symmetry and just use "apply symmetry".

This commit declare a relation and 3 TypeClasses on it:
  Reflexive
  Symmetric
  Transitive

Instances of all 3 exist for "paths" ("=") and "Equiv" ("<~>").

I changed "apply inverse" and "apply equiv_inverse" to "apply symmetry" where I found it.