proposition: Lemma validDomainName_proj2_OK : forall domain, ValidDomainName domain -> decides true (forall pre post : string, domain = (pre ++ "." ++ post)%string -> post <> ""%string /\ pre <> ""%string /\ ~ (exists s' : string, post = String "." s') /\ ~ (exists s' : string, pre = (s' ++ ".")%string)).
proof: Proof. simpl; intros; apply H; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt