proposition: Lemma AsciiToByte_ByteToAscii : forall a, (ByteToAscii (AsciiToByte a)) = a.
proof: Proof. destruct a; reflexivity. 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