proposition: Lemma WrapByte_BoundedNat8ToByte_WrapNat8_compat_1 : forall w, (wrap (BoundedNat8ToByte w) : W) = (wrap w : W).
proof: Proof. intros. unfold wrap, WrapByteIntoW. rewrite BtoW_BoundedNat8ToByte_natToWord; reflexivity. 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