HoTT/HoTT — pull request #461 by JasonGross (2014-09-06 01:21:47+00:00)
Title: 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, for now.