proposition: Lemma map_OK : forall A B (f : A -> B) dom (m : t A dom), OK dom (S.map f (proj1_sig m)).
proof: Proof. intros A B f dom m. intro x. rewrite <- (proj2_sig m x). split; intro Hin. + apply S.map_2 in Hin. assumption. + destruct Hin as [v Hv]. exists (f v). apply S.map_1. assumption. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface