proposition: Lemma resourceRecord_DecomposeRawQueryStructure_inj_inverse : forall (tup : resourceRecord), Tuple_DecomposeRawQueryStructure_inj' (qs_schema := DnsSchema) Fin.F1 (Fin.FS (Fin.FS (Fin.FS Fin.F1))) ResourceRecordTypeTypes (SumType.inj_SumType ResourceRecordTypeTypes) (SumType.SumType_index ResourceRecordTypeTypes (GetAttributeRaw tup (Fin.FS (Fin.FS (Fin.FS Fin.F1))))) (Tuple_DecomposeRawQueryStructure_proj' (qs_schema := DnsSchema) Fin.F1 (Fin.FS (Fin.FS (Fin.FS Fin.F1))) ResourceRecordTypeTypes (SumType.SumType_index ResourceRecordTypeTypes) (SumType.SumType_proj ResourceRecordTypeTypes) tup) = tup.
proof: Proof. destruct tup as [? [? [? [? [ ] ] ] ] ]; simpl. unfold Tuple_DecomposeRawQueryStructure_proj', Tuple_DecomposeRawQueryStructure_inj'; simpl. unfold GetAttributeRaw; simpl. unfold ilist2_hd, ilist2_tl; simpl. destruct prim_fst2 as [? | [? | [? | ?] ] ]; simpl; try reflexivity. Qed.
imports: Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector Coq.Lists.List Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Examples.DnsServer.DecomposeSumField Fiat.Computation.FoldComp Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema