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)