proposition: Lemma encode_list_Impl_EncodeBoundedNat_padding_0 : forall (lst: list (BoundedNat 8)) (c : CacheEncode), padding (fst (encode_list_Impl EncodeBoundedNat lst c)) = 0.
proof: Proof. intros; rewrite encode_list_as_foldl. apply fold_encode_list_body_padding_0; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega