On 2013-12-17 09:53, Sergei Meshveliani wrote: > I consider implementing AssociationList, > like AssocList in the Haskell library, only with some proofs. > > Has the Agda standard library such? Perhaps you can use Data.List.Any.any. -- /NAD