proposition: Lemma ByteString2ListOfChar_append b1 b2 : padding b1 = 0 -> padding b2 = 0 -> ByteString2ListOfChar (bin_measure (mappend b1 b2)) (mappend b1 b2) = app (ByteString2ListOfChar (bin_measure b1) b1) (ByteString2ListOfChar (bin_measure b2) b2).
proof: Proof. intros. rewrite !ByteString2ListOfChar_eq'. simpl. rewrite <- ByteBuffer_to_list_append. rewrite <- (build_aligned_ByteString_byteString_idem b1). rewrite <- (build_aligned_ByteString_byteString_idem b2). rewrite <- build_aligned_ByteString_append. f_equal. all : eauto. rewrite padding_ByteString_enqueue_aligned_ByteString; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.Option Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.InternetChecksum Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats Bedrock.Word