proposition: Theorem remove_neq_alist: forall (m : alist) (k k' : K), ~R k' k -> alist_find k (alist_remove k' m) = alist_find k m.
proof: Proof. unfold mapsto_alist. induction m; simpl; eauto; try congruence. destruct a; simpl. intros; consider (k' ?[ R ] k); simpl; intros; eauto. { consider (k0 ?[ R ] k); intros; eauto. exfalso. eapply H. etransitivity; eauto. } { consider (k0 ?[ R ] k); eauto. } 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)