proposition: Lemma constant_Some : forall A dom (v : A) x u, find x (constant dom v) = Some u <-> Dom.In x dom ∧ u = v.
proof: Proof. intros A dom v x u. unfold constant, find. simpl. rewrite Dom.fold_spec, <- Dom.elements_spec1, constant_aux. split; intro Hin. + destruct Hin; trivial. exfalso. destruct H as [_ Habs]. apply S.find_2 in Habs. revert Habs. apply S.empty_1. + left. assumption. + eapply SortA_NoDupA; refine _. apply Dom.elements_spec2. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface