proposition: Lemma Vector_checksum_eq_checksum' : forall (sz' sz : nat) (sz_lt : le sz sz') (bytes : ByteBuffer.t sz), Vector_checksum bytes = checksum (Vector.to_list bytes).
proof: Proof. induction sz'; simpl; eauto. - intros; inversion sz_lt; subst. revert bytes; apply Vector.case0; reflexivity. - intros; inversion sz_lt; subst; eauto. revert IHsz'; pattern sz', bytes; apply Vector.caseS; simpl; intros. destruct t; simpl in *; eauto. rewrite IHsz'; eauto. 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