formalize closed terms in Agda
prove correctness of addition of church numerals
use new module for reasoning about beta-reduction in agda
simplify proof of church addition by using special reduction rule for closed terms
rename constructors for Closed′
simplified proof of church addition using congruence construction
prove correctness of multiplication of church numerals