proposition: Lemma freshStringAuxSpec: forall sugg (avoid : list string) lm, !LIn (freshStringAux lm avoid sugg) avoid [+] (length (freshStringAux lm avoid sugg) = (length (shead sugg) + lm)%nat).
proof: Proof. unfold freshString. induction lm; cpx. intros. allsimpl. rewrite memberb_din. cases_ifd Hd; cpx. dorn IHlm; cpx. right. rewrite lengthAppendStr. simpl. omega. Qed.
imports: AssociationList Omega variables String Ascii