Programming in Concoqtion [DONE]

- Instead of focusing on two data-structures, we should really focus
on concepts. In fact, it would be better to start directly with saying
that we want to focus on the four programming techniques (existentials,
option types, match, and cast) and THEN saying that they will
be illustrated with examples using lists and braun trees.
- Note: We should write this section in the context of what was
already discussed in the paper. For example, where lists not
discussed at all?
- Also, the definitions of sized lists and braun trees can be
explain in section 1. We can drop the current intro/opening
of section 2. Also, it would be good to write each example
on a different line, so that they come up something like this:

Nil : (0, 'a) list
Cons (1, Nil) : (1, int) list
Cons ('a', Cons 'b', Nil) : (2, char) list

with the semi-colons aligned one on top of the other.
- For the braun trees, it might be good to insert some little
diagrams. If you want to do that, then it it would be good
to look for some latex packages for drawing small trees.
Alternatively, you can generate a high-quality pdf using an
easily available program, and we can include it in the tex
file. Generally, the first option is preferable.
- A section on existential quantification should explain in
broader terms why it would be needed in general. First, it
should start with a clear statement: While we have an explicit
construct for universal quantification at the level of types,
we do not have one for existential quantification.
Existential quantification arises natural in situations where
a function (such as a type-checker) has to produce a value with
a type that was not explicitly provided in the input.
In fact, existentials would be needed whenever we have coercsions
from values of simple types to values of more refined depedent
types (such as converting from lists to sized lists). It is
therefore
important to know how to Concoqtion can express a limited
for of existentials. The basic idea is drawn from the following
relation between existential and universal quantification:

... write equivalence here ...

- Is it really necessary to understand how things work in Coq
to understand this trick? We should keep everything as short
and as direct as possible.