proposition: Lemma ByteBuffer_checksum_checksum'' : forall {sz} (bytes: ByteBuffer.t sz) acc, ByteBuffer_fold_left16 add_w16_into_checksum sz bytes acc = checksum'' (make_pairs (Vector.to_list bytes) (wzero _)) acc.
proof: Proof. fix IH 2. destruct bytes as [ | hd sz [ | hd' sz' tl ] ]; intros; simpl. - reflexivity. - reflexivity. - unfold ByteBuffer_fold_left16 in *; simpl in *. rewrite IH. reflexivity. 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