proposition: Lemma AsciiToByte_inj : forall a1 a2, AsciiToByte a1 = AsciiToByte a2 -> a1 = a2.
proof: Proof. intros. rewrite <- (AsciiToByte_ByteToAscii a1), <- (AsciiToByte_ByteToAscii a2), H; 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