fact: Fixpoint freshStringAux (maxLen: nat) (avoid : list string) (sugg : list string) := match maxLen with | 0 => shead (sugg) | S n => let rs := freshStringAux n avoid sugg in match (memberb string_dec rs avoid) with | true => rs ++ "1" | false => rs end end.
imports: AssociationList Omega variables String Ascii