Proof of correctness of addition and multiplication of Church numerals in Agda

Hi! I was reading *Lectures on the Curry-Howard Isomorphism* and learning about Church encodings when I thought that proving their correctness would be a fun Agda exercise. Since I didn't want to start from scratch by formalizing the λ-calculus, I chose your existing project as a base. This pull requests contains my (admittedly ugly) proofs of correctness of multiplication and addition of church numerals. In some proofs, it was convenient to have some lemmas about closed terms, so I've added those.

Thanks for sharing your work!