proposition: Lemma Equiv_find_Some : forall m m', Equiv eq m m' -> forall k x, find k m = Some x -> exists x', find k m' = Some x' /\ eq x x'.
proof: Proof. intros m m' mm' k x kx. rewrite <- find_mapsto_iff in kx. destruct (Equiv_MapsTo mm' kx) as [x']. exists x'. rewrite <- find_mapsto_iff. hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)