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 a

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. :)