proposition: Lemma ByteString_pop_eq_push : forall b b' b'', ByteString_pop b = Some (b', b'') -> b = ByteString_push b' b''.
proof: Proof. destruct b; unfold ByteString_pop; simpl. destruct padding; simpl. - destruct byteString; simpl; intros. + discriminate. + injections. unfold ByteString_push; simpl. f_equal. rewrite (shatter_word front); reflexivity. eapply le_uniqueness_proof. rewrite (shatter_word c); simpl; f_equal. - intros; rewrite (shatter_word front); injections. unfold ByteString_push; simpl. destruct (Peano_dec.eq_nat_dec padding 7). subst; exfalso; omega. f_equal. eapply 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