proposition: Lemma ByteString2ListOfChar_push_char : forall n c b PaddingOK, ByteString2ListOfChar (8 + n) (ByteString_enqueue_ByteString {| front := WO; paddingOK := PaddingOK; byteString := [c] |} b) = (c :: (ByteString2ListOfChar n b))%list.
proof: Proof. Local Opaque monoid_dequeue_word. intros. simpl. replace {| padding := 0; front := WO; paddingOK := PaddingOK; byteString := [c] |} with (ByteStringToBoundedByteString (word_into_ByteString PaddingOK (c : word (0 + 1 * 8)))). rewrite monoid_dequeue_enqueue_word. reflexivity. unfold char in c; shatter_word c. reflexivity. 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