proposition: Lemma WrapByte_BoundedNat8ToByte_WrapNat8_compat: forall w : BoundedNat 8, @wrap (Value ADTValue) byte (@WrapSCA byte WrapByteIntoW) (BoundedNat8ToByte w) = @wrap (Value ADTValue) (BoundedNat 8) (@WrapSCA (BoundedNat 8) WrapNatIntoW8) w.
proof: Proof. unfold wrap, WrapSCA; intros; rewrite WrapByte_BoundedNat8ToByte_WrapNat8_compat_1; 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