proposition: Lemma update_dec : forall m m' k e, MapsTo k e (update m m') -> { MapsTo k e m' } + { MapsTo k e m /\ ~In k m'}.
proof: Proof. intros m m' k e H. rewrite update_mapsto_iff in H. destruct (In_dec m' k) as [H'|H']; [left|right]; intuition. elim H'; exists e; auto. Defined.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface