proposition: Lemma remove_remove_2 (m: t elt) x x' : remove x (remove x' m) == remove x' (remove x m).
proof: Proof. intros y. rewrite !remove_o. do 2 destruct K.eq_dec; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)