proposition: Lemma remove_other : forall A x y dom (m : t A dom), ¬X.eq y x -> find y (remove x m) = find y m.
proof: Proof. intros A x y dom [m Hok] Heq. unfold find, remove. simpl. destruct (S.find y m) as [v |] eqn:Hin. + apply S.find_1, S.remove_2, S.find_2; trivial; now symmetry. + destruct (S.find y (S.remove x m)) as [v |] eqn:Hin'; trivial. apply S.find_2, S.remove_3, S.find_1 in Hin'; auto. rewrite Hin in Hin'. discriminate Hin'. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface