A function that uses a membership proof to safely locate a tuple in a list.

locate.idr

locate : Eq a => (key : a) -> (entries : List (a, b)) -> {auto membership : Elem key (map Prelude.Basics.fst entries)} -> b
locate {membership} _ [] = absurd membership
locate {membership = Here} key ((key, value) :: _) = value
locate {membership = (There later)} key (_ :: entries) = locate key entries {membership = later}