HoTT/HoTT — pull request #141 by JasonGross (2013-07-07 16:02:52+00:00)
Title: Define [f_ap] to replace the late [f_equal]

I'm not sure exactly how [f_ap] differs from [f_equal], as I've not
looked at the ml definition of [f_equal]. I've included a fairly
lengthy comment explaining how [f_ap] works, and included a note about
generalizing it.

This closes #139.