6.4.2 isn't using funext, close #640
errata for ec1373a
Merge pull request #643 from mikeshulman/lemma6.4.2

6.4.2 isn't using funext, close #640