proposition: Lemma remove_OK : forall A dom x (m : t A dom), OK (Dom.remove x dom) (S.remove (elt:=A) x (proj1_sig m)).
proof: Proof. destruct m as [m Hok]. simpl. intro y. split; intro Hin. + destruct (X.eq_dec x y) as [Hxy | Hxy]. - elim (S.remove_1 Hxy Hin). - rewrite Dom.remove_spec. destruct Hin as [u Hy]. apply S.remove_3 in Hy. rewrite <- (Hok y). split. now exists u. now symmetry. + rewrite Dom.remove_spec in Hin. destruct Hin as [Hin Hxy]. rewrite <- (Hok y) in Hin. destruct Hin as [u Hin]. exists u. apply S.remove_2; trivial. now symmetry. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface