proposition: Lemma is_empty_spec : forall A dom (m : t A dom), is_empty m = true <-> forall x, find x m = None.
proof: Proof. unfold find, is_empty. intros A dom [m Hok]. simpl. split; intro Hempty. + intro x. destruct (S.find x m) as [v |] eqn:?; trivial. assert (Habs : S.In x m) by now exists v; apply S.find_2. rewrite (Hok x) in Habs. rewrite Dom.equal_spec in Hempty. fsetdec. + apply Dom.equal_spec, DProp.MP.empty_is_empty_1. intros x Habs. rewrite <- (Hok x) in Habs. destruct Habs as [v Habs]. apply S.find_1 in Habs. rewrite Hempty in Habs. discriminate Habs. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface