proposition: Lemma add_same : forall A x v dom (m : t A dom), find x (add x v m) = Some v.
proof: Proof. intros ? ? ? ? [? ?]. unfold add, find. simpl. apply S.find_1, S.add_1. reflexivity. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface