proposition: Lemma WrapNatIntoW_le32_inj {size}: (size <= 32) -> forall v v' : BoundedNat size, (natToWord 32 (` v)) = (natToWord 32 (` v')) -> v = v'.
proof: Proof. intros; apply natToWord_inj in H0; eauto using exist_irrel', lt_uniqueness_proof, BoundedNat_below_pow2__le32. 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