fact: Fixpoint StringToByteString s := match s with | EmptyString => nil | String hd tl => cons (AsciiToByte hd) (StringToByteString tl) end.
imports: Coq.Program.Program Fiat.CertifiedExtraction.Core Fiat.CertifiedExtraction.FacadeWrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Bedrock.Arrays Bedrock.Platform.Facade.examples.QsADTs Bedrock.Word