WellFounded TreeMap

Stream: new members

[Ka Wing Li]

I am trying to port the proof from https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.stringmap.html. Basically, I need to do induction on the well-formedness of TreeMap. Is there any way to do so? I want to induct on the size of the map.

abbrev StringMap (α : Type) := TreeMap.Raw String α

abbrev R {α} (s : String) (m : StringMap α) (n₁ n₂ : ℕ) : Prop :=
  n₂ < n₁ ∧ m[s ++ toString (n₁ - 1)]?.isSome

theorem fresh_string_R_wf {α} (s : String) (m : StringMap α) : WellFounded (R s m) := by
  -- induction (map_wf m)
  sorry