proposition: Lemma update_spec1 (f:option elt->option elt) m x : find x (update x f m) = f (find x m).
proof: Proof. unfold update. destruct f; [apply add_spec1 | apply remove_spec1]. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)