proposition: Lemma update_in_iff : forall m m' k, In k (update m m') <-> In k m \/ In k m'.
proof: Proof. intros m m' k. split. - intros (e,H); rewrite update_mapsto_iff in H. destruct H; [right|left]; exists e; intuition. - destruct (In_dec m' k) as [H|H]. + destruct H as (e,H). intros _; exists e. rewrite update_mapsto_iff; left; auto. + destruct 1 as [H'|H']; [|elim H; auto]. destruct H' as (e,H'). exists e. rewrite update_mapsto_iff; right; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface