proposition: Lemma add_OK : forall A dom x v (m : t A dom), OK (Dom.add x dom) (S.add x v (proj1_sig m)).
proof: Proof. destruct m as [m Hok]. simpl. intro y. split; intro Hin. + destruct Hin as [u Hy]. destruct (X.eq_dec x y) as [Hxy | Hxy]. - fsetdec. - rewrite Dom.add_spec. right. rewrite <- (Hok y). apply S.add_3 in Hy; trivial. exists u. assumption. + rewrite Dom.add_spec in Hin. destruct (X.eq_dec x y) as [Hxy | Hxy]. - exists v. apply S.add_1. assumption. - destruct Hin as [Hin | Hin]; try now symmetry in Hin; contradiction. rewrite <- (Hok y) in Hin. destruct Hin as [u Hy]. exists u. apply S.add_2; assumption. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface