proposition: Theorem mapsto_lookup_alist : forall (k : K) (v : V) (m : list (K * V)), lookup k m = Some v <-> mapsto_alist m k v.
proof: Proof. reflexivity. Qed.
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)