proposition: Lemma find_mapsto_equiv : forall m m' x, bst m -> bst m' -> (find x m = find x m' <-> (forall d, MapsTo x d m <-> MapsTo x d m')).
proof: Proof. intros m m' x Hm Hm'. rewrite find_find. split; intros H d; specialize H with d. - rewrite <- 2 find_iff; auto. - rewrite 2 find_iff; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int