proposition: Lemma ByteString_transform_length : forall str1 str2, padding str1 = 0 -> padding str2 = 0 -> List.length (byteString (transform str1 str2)) = List.length (byteString str1) + List.length (byteString str2).
proof: Proof. unfold transform, ByteStringTransformer; intros. rewrite ByteString_transformer_eq_app by assumption; simpl. rewrite app_length; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega