proposition: Lemma set_same : forall A x v dom (m : t A dom) Hin, find x (@set A dom x v m Hin) = Some v.
proof: Proof. intros. unfold set, find. simpl. apply S.find_1, S.add_1. reflexivity. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface