proposition: Lemma extend_mapsto_iff : forall m m' k e, MapsTo k e (extend m m') <-> (MapsTo k e m' \/ (MapsTo k e m /\ ~In k m')).
proof: Proof. unfold extend. intros m m'. pattern m', (fold (@add _) m' m). apply fold_rec. - intros m0 Hm0 k e. assert (~In k m0) by (intros (e0,He0); apply (Hm0 k e0); auto). intuition. elim (Hm0 k e); auto. - intros k e m0 m1 m2 _ Hn Hadd IH k' e'. change (m2 == add k e m1) in Hadd. rewrite Hadd, 2 add_mapsto_iff, IH, add_in_iff. clear IH. intuition. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)