proposition: Lemma WrapN_le32_inj {av} {size}: (size <= 32) -> forall v v' : BoundedN size, wrap (FacadeWrapper := @FacadeWrapper_SCA av) (NToWord 32 (` v)) = wrap (FacadeWrapper := @FacadeWrapper_SCA av) (NToWord 32 (` v')) -> v = v'.
proof: Proof. intros; rewrite !NToWord_nat in H0. apply wrap_inj, natToWord_inj, N2Nat.inj in H0; eauto using exist_irrel', UipComparison.UIP, BoundedN_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