Library Coq.Program.Combinators
Proofs about standard combinators, exports functional extensionality.
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France
Composition has id for neutral element and is associative.
flip is involutive.
prod_curry and prod_uncurry are each others inverses.