proposition: Lemma GetAttributeRaw_FS : forall {A} {heading} (a : A) (tup : @RawTuple heading) n, @GetAttributeRaw {| AttrList := Vector.cons _ A _ (AttrList heading) |} {| prim_fst := a; prim_snd := tup |} (Fin.FS n) = GetAttributeRaw tup n.
proof: Proof. unfold GetAttributeRaw; simpl; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Compose Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Lib2.WordOpt Fiat.Narcissus.Lib2.NatOpt Fiat.Narcissus.Lib2.StringOpt Fiat.Narcissus.Lib2.EnumOpt Fiat.Narcissus.Lib2.FixListOpt Fiat.Narcissus.Lib2.SumTypeOpt Fiat.Common.SumType Fiat.Examples.Tutorial.Tutorial Fiat.Examples.DnsServer.DecomposeEnumField 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.Examples.HACMSDemo.DuplicateFree Fiat.QueryStructure.Automation.MasterPlan Bedrock.Word Bedrock.Memory