The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Arnaud, Thank you. The notion that it's reasonable to force one who wishes to program to "reprove" theorems with opaque proof terms makes sense, given that proofs are in general produced without regard for efficiency. I understand the philosophy. (It raises an interesting, probably academic, thought, though: might one reprove the entire Coq library to provide "efficient" proofs, leaving them all transparent, and thus useful as a kind of reusable library of programming codes. (I don't mean or propose to pursue this idea.) Thanks, again, for your feedback.

Kevin  

On Tue, Nov 26, 2013 at 12:54 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

singleton elimination of equality