Agda.Utils.Empty
data
Empty
absurd