proposition: Theorem mapsto_add_neq_alist : forall (m : list (K * V)) (k : K) (v : V), forall k', ~ R k k' -> forall v', (mapsto_alist m k' v' <-> mapsto_alist (add k v m) k' v').
proof: Proof. unfold mapsto_alist, add; simpl. intros. consider (k' ?[ R ] k); try solve [ intros; exfalso; auto ]. intros. eapply mapsto_remove_neq_alist in H. eapply H. 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)