Examples that show paradoxes when using combinations of impredicative polymorphism + excluded middle + large elimination -- can only choose two

Since this is an important discussion I'm splitting off a separate thread (previous one is https://github.com/FStarLang/FStar/issues/355#issuecomment-139806214).

It is folklore in the type theory world that mixing the following, very useful and apparently innocuous, ingredients leads to inconsistency:

```
impredicative polymorphism + excluded middle + large elimination => false
```

In particular, Berardi's paradox (the latest of a series of paradoxes starting with Russell's paradox) shows that

```
(1) impredicative polymorphism + excluded middle => proof irrelevance
```

Proof irrelevance says that all proofs of the same proposition are equal, or more generally that all inhabitants of the same type are equal. Proof irrelevance is a reasonable property, for instance Coq's sort `Prop` is impredicative and known to soundly admit proof irrelevance (and excluded middle too). Proof irrelevance is, however, clearly incompatible with anything that would allow distinguishing proofs, or generally type inhabitants. "Large elimination" is such a thing.

```
(2) proof irrelevance + large elimination => false
```

Coq enforces that values of types of sort `Prop` are not used for their informational content by imposing an **elimination restriction**: if a match expression matches on a value of a type of sort `Prop`, the return type of the match expression must itself also be of sort `Prop`. In other words, matching on proofs is allowed only to build other proofs.
This restriction is strong. In particular, if `Bool` was defined in `Prop`, this restriction would prevent one from proving that true and false are distinct:

``` coq
Inductive Bool : Prop := T : Bool | F : Bool.

Definition two_elements_Bool (H : T = F) : False :=
match H in (_ = y0) return (match y0 with
| T => True
| F => False
end) with
| eq_refl => I
end.
(* Error: *)
(* Incorrect elimination of "y0" in the inductive type "Bool": *)
(* the return type has sort "Type" while it should be "Prop". *)
(* Elimination of an inductive object of sort Prop *)
(* is not allowed on a predicate in sort Type *)
(* because proofs can be eliminated only to build proofs. *)
```

As we see more pressure to deeply integrate classical proofs done with the SMT solver with manual constructive proofs in F*'s pure fragment, splitting up a separate kind `Prop`, that's a sub-kind of `Type` and that features impredicative polymorphism and excluded middle seems appealing. The key to doing this soundly seems adopting Coq's elimination restriction for `Prop`.

Summoning @nikswamy, @ckeller, @s-zanella, @aa755, and @maximedenes for this discussion.

**Some references**
https://cstheory.stackexchange.com/questions/21836/why-does-coq-have-prop/21878#21878
http://people.cs.kuleuven.be/~bart.jacobs/coq-essence.pdf (Section 13 discusses sort Prop)
https://coq.inria.fr/refman/Reference-Manual006.html#sec208
http://adam.chlipala.net/cpdt/html/Universes.html#lab77
https://coq.inria.fr/library/Coq.Logic.Berardi.html
https://github.com/FStarLang/FStar/blob/master/examples/paradoxes/berardi_minimal.fst
http://www.cs.nott.ac.uk/~txa/g53cfr/l20.html/l20.html