proposition: Lemma length_encode_word' sz : forall (w : word sz) (b : ByteString), bin_measure (encode_word' _ w b) = sz + bin_measure b.
proof: Proof. simpl; intros. rewrite <- length_encode_word' with (w := w). induction sz; intros; rewrite (shatter_word w); simpl. - reflexivity. - reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Narcissus.BinLib Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Automation.NormalizeFormats Bedrock.Word