absurdity : Uninhabited t => (0 _ : t) -> s
contradiction : Uninhabited t => (0 _ : (x -> t)) -> x -> s