proposition: Lemma fold_rec_nodep : forall (A:Type)(P : A -> Type)(f : key -> elt -> A -> A)(i:A)(m:t elt), P i -> (forall k e a, MapsTo k e m -> P a -> P (f k e a)) -> P (fold f m i).
proof: Proof. intros; apply fold_rec_bis with (P:=fun _ => P); auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface