proposition: Lemma length_encode_word' sz : forall (w : word sz) (b : ByteString), bin_measure (encode_word' _ w b) = sz + bin_measure b.
proof: Proof. induction sz; intros; rewrite (shatter_word w); simpl. - reflexivity. - pose proof measure_enqueue as H'; simpl in H'. unfold encode_word in *; simpl in *. rewrite <- (ByteStringToBoundedByteString_BoundedByteStringToByteString_eq (ByteString_enqueue _ _)). rewrite length_ByteString_ByteStringToBoundedByteString_eq. rewrite <- ByteString_enqueue_ByteStringToBoundedByteString_eq'. rewrite length_ByteString_enqueue. rewrite <- length_ByteString_ByteStringToBoundedByteString_eq. rewrite ByteStringToBoundedByteString_BoundedByteStringToByteString_eq. erewrite <- IHsz. 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