Add proof for ex3_eta
Add proof that eta is substitutive
Simplify eta substitutive proof
Add some lemmas about eta
Add parallel beta and some related lemmas
Add proof that eta_par is reflexive
Change definition of lam_k and simplify proofs
Add module for the eta-postponement theorem
Merge pull request #15 from knuton/postponement

Postponement