proposition: Lemma remove_neq_o : forall m x y, ~ E.eq x y -> find y (remove x m) = find y m.
proof: Proof. intros. rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff, remove_neq_mapsto_iff; now intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface