proposition: Lemma monoid_dequeue_enqueue_word : forall (w : word (0 + 1 * 8)) (ext : ByteString) OK, monoid_dequeue_word _ (ByteString_enqueue_ByteString (ByteStringToBoundedByteString (word_into_ByteString OK w)) ext) = (w, ext).
proof: Proof. simpl; intros; shatter_word w. unfold word_into_ByteString; simpl. do 8 match goal with |- context [ByteString_dequeue (ByteString_enqueue_ByteString ?z _)] => let H := fresh in destruct (ByteString_dequeue z) as [ [? ?] | ] eqn:H; unfold ByteString_dequeue in H; simpl in H; [ erewrite ByteString_dequeue_mappend_opt; try eassumption; injections | discriminate ]; match goal with |- context [ {| padding := _; front := _; paddingOK := ?H; byteString := _ |} ] => generalize H; intros; simpl end end. repeat f_equal. pose proof (mempty_left ext) as H7; simpl in H7; rewrite <- H7 at -1. unfold ByteString_id; repeat f_equal. apply le_uniqueness_proof. 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