LCC(Lambda calculus on Coq) OVERVIEW LCC is a implementation of simple typed lambda calculus. And some theorems. PREREQUIRED Coq 8.2p1 or latter omake PROOF $ omake AUTHOR MIZUNO "mzp" Hiroki (mzp@ocaml.jp)