proposition: Lemma for_all_iff : forall m, for_all f m = true <-> (forall k e, MapsTo k e m -> f k e = true).
proof: Proof. unfold for_all. set (f':=fun k e b => if f k e then b else false). intro m. pattern m, (fold f' m true). apply fold_rec. - intros m' Hm'. split; auto. intros _ k e Hke. elim (Hm' k e); auto. - intros k e b m1 m2 _ Hn Hadd IH. clear m. change (Equal m2 (add k e m1)) in Hadd. unfold f'; simpl. case_eq (f k e); intros Hfke. + rewrite IH. clear IH. split; intros Hmapsto k' e' Hke'. * rewrite Hadd, add_mapsto_iff in Hke'. destruct Hke' as [(?,?)|(?,?)]; auto. rewrite <- Hfke; apply Hf; auto. * apply Hmapsto. rewrite Hadd, add_mapsto_iff; right; split; auto. contradict Hn; exists e'; rewrite Hn; auto. + split; try discriminate. intros Hmapsto. rewrite <- Hfke. apply Hmapsto. rewrite Hadd, add_mapsto_iff; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface