Utilities for working with uninhabited types, to record explicit

locations for canonical proofs of emptiness. Typically, one should

use the `absurd`

function.

- absurd : Uninhabited t => (h : t) -> a
Use an absurd assumption to discharge a proof obligation

- a
the goal type

- t
some empty type

- h
the contradictory hypothesis

- interface Uninhabited
A canonical proof that some type is empty

- uninhabited : Uninhabited t => t -> Void
If I have a t, I've had a contradiction