proposition: Lemma freshStringSpec: forall (avoid : list string) sugg, !LIn (freshString avoid sugg) avoid.
proof: Proof. unfold freshString. intros. pose proof (freshStringAuxSpec sugg avoid (S (lmax (map length avoid) - length (shead sugg)))) as Hfs. dorn Hfs; cpx. fold (freshString avoid sugg). fold (freshString avoid sugg) in Hfs. assert (length (shead sugg) + S (lmax (map length avoid) - length (shead sugg)) > (lmax (map length avoid))) as XX by omega. rewrite <- Hfs in XX. introv Hc. apply lmaxSpecLen in Hc. omega. Qed.
imports: AssociationList Omega variables String Ascii