proposition: Lemma Vector_checksum_bound_acc' : forall sz'' sz sz' (sz_lt : le sz' sz'') (v : Vector.t _ sz) b1 b2 acc, Vector_checksum_bound sz' v (add_bytes_into_checksum b1 b2 acc) = add_bytes_into_checksum b1 b2 (Vector_checksum_bound sz' v acc).
proof: Proof. induction sz''; intros. - inversion sz_lt. subst; reflexivity. - inversion sz_lt; subst. + clear sz_lt. destruct sz''; simpl. * destruct v; simpl; eauto. rewrite add_bytes_into_checksum_swap; eauto. * destruct v; simpl; eauto. destruct v; simpl; eauto. rewrite add_bytes_into_checksum_swap; eauto. rewrite !IHsz'' by omega. rewrite add_bytes_into_checksum_swap; eauto. + eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith 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.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Stores.EmptyStore Bedrock.Word