proposition: Lemma resourceRecordOK_3 : forall rr : resourceRecord, resourceRecord_OK rr -> ith (icons (B := fun T => T -> Prop) (fun a : DomainName => ValidDomainName a) (icons (B := fun T => T -> Prop) (fun _ : Memory.W => True) (icons (B := fun T => T -> Prop) (fun a : DomainName => ValidDomainName a) (icons (B := fun T => T -> Prop) (fun a : SOA_RDATA => (True /\ ValidDomainName a!"contact_email") /\ ValidDomainName a!"sourcehost") (icons (B := fun T => T -> Prop) (fun a : WKS_RDATA => True /\ (lt (|a!"Bit-Map" |) (pow2 16))) (icons (B := fun T => T -> Prop) (fun a : DomainName => ValidDomainName a) (icons (B := fun T => T -> Prop) (fun a : HINFO_RDATA => (True /\ True /\ (lt (String.length a!"OS") (pow2 8))) /\ True /\ (lt (String.length a!"CPU") (pow2 8))) (icons (B := fun T => T -> Prop) (fun a : MINFO_RDATA => (True /\ ValidDomainName a!"eMailBx") /\ ValidDomainName a!"rMailBx") (icons (B := fun T => T -> Prop) (fun a : MX_RDATA => True /\ ValidDomainName a!"Exchange") (icons (B := fun T => T -> Prop) (fun a : string => True /\ True /\ (lt (String.length a) (pow2 8))) inil)))))))))) (SumType_index ResourceRecordTypeTypes rr!sRDATA) (SumType_proj ResourceRecordTypeTypes rr!sRDATA).
proof: Proof. intros ? H; apply H. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.DNSPacket Bedrock.Word