proposition: Lemma ValidDomainName_app : forall label subdomain, ValidLabel label -> ValidDomainName (label ++ (String "." subdomain)) -> ValidDomainName subdomain.
proof: Proof. unfold ValidDomainName; split; intros. - eapply H0; try eassumption. rewrite H1. change (String "." (pre ++ label0 ++ post)%string) with ((String "." pre) ++ label0 ++ post)%string. rewrite append_assoc. reflexivity. - destruct H0; subst. destruct (H2 (label ++ String "." pre)%string post) as [? [? [? ?] ] ]. rewrite <- !append_assoc; f_equal. repeat split; eauto. intro; apply H5; subst. eexists; simpl; eauto. intro; apply H5; subst. destruct_ex; subst. eexists (label ++ String "." x)%string; simpl; eauto. rewrite <- !append_assoc; 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