proposition: Theorem fold_rec_bis : forall {A}(P : t elt -> A -> Type)(f : key -> elt -> A -> A), forall i m, (forall m m' a, m == m' -> P m a -> P m' a) -> (P empty i) -> (forall k e a m', MapsTo k e m -> ~In k m' -> P m' a -> P (add k e m') (f k e a)) -> P m (fold f m i).
proof: Proof. intros A P f i m Pmorphism Pempty Pstep. apply fold_rec; intros. apply Pmorphism with empty; auto. intro k. rewrite empty_o. case_eq (find k m0); auto; intros e'; rewrite <- find_mapsto_iff. intro H'; elim (H k e'); auto. apply Pmorphism with (add k e m'); try intro; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)