proposition: Lemma Equiv_MapsTo : forall m m', Equiv eq m m' -> forall k x, MapsTo k x m -> exists x', MapsTo k x' m' /\ eq x x'.
proof: Proof. intros m m' [h1 h2] k x kx. unfold In in h1. assert (exists e, MapsTo k e m). exists x. hyp. rewrite h1 in H. destruct H as [x']. exists x'. intuition. apply h2 with k; hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)