proposition: Lemma mapsto_alist_cons : forall k v m k' v', mapsto_alist ((k',v') :: m) k v <-> ( (mapsto_alist m k v /\ ~R k k') \/ (R k k' /\ v = v')).
proof: Proof. unfold mapsto_alist; intuition; simpl in *. { consider (k ?[ R ] k'); intros. { right. inversion H0; auto. } { left. auto. } } { consider (k ?[ R ] k'); intros; intuition. } { consider (k ?[ R ] k'); intros; intuition. congruence. } 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)