0 | module Data.Void 1 | 2 | export 3 | absurdity : Uninhabited t => (0 _ : t) -> s 4 | absurdity x = void (uninhabited x) 5 | 6 | export 7 | contradiction : Uninhabited t => (0 _ : x -> t) -> (x -> s) 8 | contradiction since x = absurdity (since x) 9 |