dogsleg/lia — pull request #1 by yfcai (2013-07-15 09:15:42+00:00)
Title: distributivity∧∨ and my take on question 3 by example

Hi Lev,

I like your formulation of intuitionistic logic in Agda. Seeing the introduction and elimination forms used "for real" in Agda improves my understanding of their pen/paper presentation we saw in the seminar at the beginning of this semester.

This pull request contains a proof of `distributivity∧∨` close to how I'd phrase it on paper and an attempt at answering your third question on how to phrase axioms about quantifiers. Hope they'd help. If you have further topics about the lia repository for discussion, I'd be glad to participate.

Modifications:

- extracting from `Exists A B` the term `t : A` for which `B t` holds
- proof of distributivity∧∨
- axiom₁₁, another form of ∀-elimination
- axiom₁₃, Kleene's existence property (ED)