fact: Definition fresh_string_go {A} (s : string) (m : stringmap A) (n : N) (go : ∀ n', R s m n' n → string) : string := let s' := s +:+ pretty n in match Some_dec (m !! s') with | inleft (_↾Hs') => go (1 + n)%N (fresh_string_step s m n _ Hs') | inright _ => s' end.
imports: stdpp(gmap) stdpp(options)