proposition: Theorem remove_eq_alist: forall (m : alist) (k : K), alist_find k (alist_remove k m) = None.
proof: Proof. unfold mapsto_alist. induction m; simpl; eauto; try congruence. intros; consider (k ?[ R ] fst a); simpl; intros; eauto. destruct a; simpl in *. consider (k ?[ R ] k0); eauto. tauto. 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)