proposition: Lemma Vector_checksum_ByteBuffer_checksum : forall {sz} (bytes: ByteBuffer.t sz), Vector_checksum bytes = ByteBuffer_checksum bytes.
proof: Proof. intros. rewrite Vector_checksum_eq_checksum, checksum_checksum'. unfold ByteBuffer_checksum, ByteBuffer_checksum_bound; rewrite ByteBuffer_checksum_checksum''. apply checksum'_checksum''. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing Program Coq.micromega.Psatz AlignedByteString Permutation