proposition: Lemma ByteToAscii_AsciiToByte : forall b, (AsciiToByte (ByteToAscii b)) = b.
proof: Proof. intros; unfold ByteToAscii. shatter_word b; 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