Soundness: ensure datatypes are inhabited

[joscoh]

Now that the destructors are automatically generated per datatype, it is important to ensure that every type is inhabited, or else we can generate inconsistent axioms. For example:

datatype Empty
datatype List = Nil | Cons (hd: Empty) (tl: List)

generates the destructor hd: List -> Empty, which can be used to produce an instance of type Empty. To fix this, we need a proper check to ensure that datatypes are inhabited.