proposition: Lemma singleton_other : forall A x y (v : A), ¬X.eq y x -> find y (singleton x v) = None.
proof: Proof. intros A x y v Heq. unfold singleton, find. simpl. destruct (S.find y (S.add x v (S.empty A))) as [u |] eqn:Hin; trivial. apply S.find_2, S.add_3 in Hin. elim (S.empty_1 Hin). now symmetry. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface