Finmap and computable map

Stream: general

[Ka Wing Li]

Is there any way to relate Finmap and other computable maps, such as TreeMap and HashMap? So that I can reuse the lemmas or well-founded induction in Finmap on algorithms using TreeMap?