coq/coq — pull request #30 by JasonGross (2014-07-31 20:37:30+00:00)
Title: Prove forall extensionality

I was surprised this wasn't in the standard library already. Apologies if it actually is, and I just missed it.