fact: Fixpoint alist_find (k : K) (m : alist) : option V := match m with | nil => None | (k',v) :: ms => if k ?[ R ] k' then Some v else alist_find k ms end.
imports: Coq.Classes.RelationClasses Coq.Lists.List ExtLib.Core.RelDec ExtLib.Tactics.Consider ExtLib.Structures.Maps ExtLib.Structures.Monad ExtLib.Structures.Reducible ExtLib.Structures.Functor Coq(Basics) ExtLib(Extras OptionMonad)