Mastodawn

A type is true if you can instantiate it, flase / empty if you can't
#GADT supports dependent types

Empty inductive type
Not A : A => F, in intuitionist logic

This is proof by contradiction

Bools =/= preposition in #coq
Not provable =/= false