Idris2Doc : Data.Void

Data.Void

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