I find lambda calculus needed when you get into some of the subjects that functional programming languages are a gateway to. It definitely helps when trying to read the Coq manual.