Standard functions and combinators.
Proofs about them require functional extensionality and can be found
in
Combinators.
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - University Paris Sud
The polymorphic identity function is defined in
Datatypes.
Function composition.
Logical implication.
Application as a combinator.