fact: Fixpoint fresh_strings_of_set (s : string) (n : nat) (X : stringset) : list string := match n with | 0 => [] | S n => let x := fresh_string_of_set s X in x :: fresh_strings_of_set s n ({[ x ]} ∪ X) end%nat.
imports: stdpp(gmap) stdpp(options)