proposition: Lemma set_OK : forall A dom x v (m : t A dom), Dom.In x dom -> OK dom (S.add x v (proj1_sig m)).
proof: Proof. destruct m as [m Hok]. intros Hx y. simpl. destruct (X.eq_dec y x) as [Hxy | Hxy]. + split; intro Hin. - rewrite Hxy. assumption. - exists v. apply S.add_1. symmetry. assumption. + split; intro Hin. - destruct Hin as [v' Hin]. rewrite <- (Hok y). exists v'. eapply S.add_3. symmetry. eassumption. eassumption. - rewrite <- (Hok y) in Hin. destruct Hin as [v' Hin]. exists v'. eapply S.add_2. symmetry. assumption. trivial. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface