proposition: Lemma WrapBoundedList_inj {A B : Type} {size : nat} {Wrp : FacadeWrapper A (list B)}: forall (v v' : BoundedList B size), wrap (` v) = wrap (` v') -> v = v'.
proof: Proof. intros * H; apply wrap_inj, WrapBoundedList_inj_1 in H; 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