proposition: Lemma StringToByteString_inj : forall s1 s2, StringToByteString s1 = StringToByteString s2 -> s1 = s2.
proof: Proof. induction s1; destruct s2; repeat match goal with | _ => congruence | _ => progress intros | _ => progress simpl in * | _ => progress f_equal | _ => solve [eauto using AsciiToByte_inj] | [ H: cons _ _ = cons _ _ |- _ ] => inversion H; subst; clear H end. 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