Agda.Utils.IndexedList
data Some
withSome
data All
makeAll
forgetAll
data Index
forgetIndex
mapWithIndex
lIndex
lookupIndex
allIndices