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