Fix V.v to work with current trunk

The [apply path_singleton] was very, very dubious.  It assumed that Coq
would apply [V_singleton u = V_singleton v <-> u = v] as [u = v ->
V_singleton u = V_singleton v].  This is not the case in 8.4, nor in
current trunk.  It's now a much simpler [apply ap].  (Is there a reason
that we weren't just using [apply ap] here?)  I've replaced
[path_singleton] with [isequiv_ap_V_singleton].

We should probably fix [path_pair_ord] as well, so that we never [apply]
an [iff], but since it only broke in one place, I just inserted an
[apply ap] there, fore now.