[foopdoopfoop]

Reminds me of Coq's definition of `False`:

`Inductive False := .`

i.e., `False` has no constructors and hence is an empty type.

Anyway, this means that for any type `A`, you can construct a function of type `False -> A` because you just do this:

`fun (x : False) => match x with end.`

Since `False` has no constructors, a match statement on a value of type `False` has no cases to match on, and you're done. (Coq's type system requires a case for each constructor of the type of the thing being matched on.) This is why, if you assume something that is false, you can prove anything. :)

[erk__]

That is made that way to mirror how logic usually is made to work in propositional logic.