proposition: Lemma WrapBoundedList_inj_1: forall (B : Type) (size : nat) (v v' : BoundedList B size), ` v = ` v' -> v = v'.
proof: Proof. intros. apply exist_irrel'. - intros; apply lt_uniqueness_proof. - eassumption. 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