proposition: Corollary checksum_eq_Vector_checksum : forall (bytes : list (word 8)), checksum bytes = Vector_checksum (Vector.of_list bytes).
proof: Proof. intros; rewrite Vector_checksum_eq_checksum, Vector.to_list_of_list_opp; 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