proposition: Lemma map_spec : forall A B (f : A -> B) dom (m : t A dom) x v, find x (map f m) = Some v <-> exists u, find x m = Some u ∧ f u = v.
proof: Proof. intros A B f dom m x v. unfold find, map. simpl. split; intro Hin. + assert (Hf : S.In x (S.map f (proj1_sig m))). { exists v. apply S.find_2. assumption. } apply S.map_2 in Hf. destruct Hf as [u Hu]. exists u. split. - apply S.find_1. assumption. - eapply S.map_1, S.find_1 in Hu. erewrite Hu in Hin. inversion Hin. reflexivity. + destruct Hin as [u [Hu Heq]]. subst. apply S.find_1, S.map_1, S.find_2. assumption. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface