proposition: Lemma fold_rec_weak : forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A)(i:A), (forall m m' a, Equal m m' -> P m a -> P m' a) -> P (empty _) i -> (forall k e a m, ~In k m -> P m a -> P (add k e m) (f k e a)) -> forall m, P m (fold f m i).
proof: Proof. intros; apply fold_rec_bis; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface