proposition: Theorem mapsto_remove_eq_alist : forall (m : list (K * V)) (k : K) (v : V), ~mapsto_alist (remove k m) k v.
proof: Proof. unfold mapsto_alist, remove, alist_remove; simpl. intros. induction m; simpl; auto. { congruence. } { destruct a; simpl in *. consider (k ?[ R ] k0); auto; intros. simpl. consider (k ?[ R ] k0); auto. } 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)