proposition: Lemma WrapNat_le32_inj {av} {size}: (size <= 32) -> forall v v' : BoundedNat size, wrap (FacadeWrapper := @FacadeWrapper_SCA av) (natToWord 32 (` v)) = wrap (FacadeWrapper := @FacadeWrapper_SCA av) (natToWord 32 (` v')) -> v = v'.
proof: Proof. intros * ? * H; apply wrap_inj in H. apply WrapNatIntoW_le32_inj; assumption. 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