proposition: Lemma singleton_OK : forall A x v, OK (Dom.singleton x) (S.add x v (S.empty A)).
proof: Proof. intros A x v y. split; intro Hin. + destruct (X.eq_dec y x) as [Hxy | Hxy]. - fsetdec. - destruct Hin as [u Hin]. apply S.add_3 in Hin. elim (S.empty_1 Hin). symmetry. assumption. + rewrite Dom.singleton_spec in Hin. exists v. apply S.add_1. symmetry; assumption. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface