proposition: Lemma remove_same : forall A x dom (m : t A dom), find x (remove x m) = None.
proof: Proof. intros A x dom [m Hok]. unfold remove, find. simpl. destruct (S.find x (S.remove x m)) as [v |] eqn:Hin; trivial. apply S.find_2 in Hin. eelim S.remove_1. reflexivity. exists v. eassumption. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface