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