proposition: Lemma update_spec2 (f:option elt->option elt) m x y : ~K.eq x y -> find y (update x f m) = find y m.
proof: Proof. intros NE. unfold update. destruct f; [apply add_spec2 | apply remove_spec2]; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)