I'm working through some intro-level combinatory logic exercises using Coq. I've written a crude library for it, but it isn't very efficient. Is there a combinatory logic library for Coq or other proof assistants? Definitions of combinators, terms & their relations along with proofs of some important theorems would be quite helpful.
There is a discussion about Agda and combinatory logic that looks interesting, but I can't tell whether it is relevant for my question.