proposition: Lemma ByteAligned_packetDecoderImpl'_OK {A} : forall (f : _ -> A) n (v : Vector.t _ (12 + n)), f (fst packetDecoderImpl (build_aligned_ByteString v) (Some (wzero 17), @nil (pointerT * string))) = ByteAligned_packetDecoderImpl' f n v (Some (wzero 17) , @nil (pointerT * string))%list.
proof: Proof. intros. pose proof (projT2 (ByteAligned_packetDecoderImpl f n)); cbv beta in H. rewrite H. set (H' := (Some (wzero 17), @nil (pointerT * string))). simpl. unfold ByteAligned_packetDecoderImpl'. reflexivity. 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.List.ListFacts Fiat.Common.StringFacts Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedSumType Fiat.Narcissus.BinLib.AlignedDomainName 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.SimpleDNSPacket Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.HintDbExtra Fiat.Common.Tactics.TransparentAbstract Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Stores.DomainNameStore Fiat.Narcissus.Automation.CacheEncoders Bedrock.Word