Add the following to Agda implementation of intuitionistic logic:
- ∀-elimination
- extracting from `Exists A B` the term `t : A` for which `B t` holds
- proof of distributivity∧∨
- axiom₁₃, Kleene's existence property (ED)
Merge pull request #1 from yfcai/master

distributivity∧∨ and my take on question 3 by example