proposition: Lemma singleton_same : forall A x (v : A), find x (singleton x v) = Some v.
proof: Proof. intros. unfold singleton, find. simpl. apply S.find_1, S.add_1. reflexivity. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface