proposition: Lemma WrapListByte_inj {capacity} : forall v v' : byteString, ByteString capacity v = ByteString capacity v' -> v = v'.
proof: Proof. inversion 1; eauto. Qed.
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