fact: Definition fresh_string {A} (s : string) (m : stringmap A) : string := match m !! s with | None => s | Some _ => Fix_F _ (fresh_string_go s m) (wf_guard 32 (fresh_string_R_wf s m) 0) end.
imports: stdpp(gmap) stdpp(options)