proposition: Theorem lt_uniqueness_proof : forall (n m : nat) (p q : n < m), p = q.
proof: Proof. unfold lt. intros; apply Core.le_uniqueness_proof. 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