proposition: Theorem mapsto_add_eq_alist : forall (m : list (K * V)) (k : K) (v : V), mapsto_alist (add k v m) k v.
proof: Proof. unfold mapsto_alist, add, alist_add; simpl. intros. consider (k ?[ R ] k); auto. intro. exfalso. apply H. 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)