proposition: Lemma CorrectAlignedEncoderForFormatMChar_f n {S} (addE_addE_plus : forall ce n m, addE (addE ce n) m = addE ce (n + m)) (addE_0 : forall ce, addE ce 0 = ce) (proj : S -> word (n * 8)) : CorrectAlignedEncoder (Projection_Format format_word proj) (fun sz v idx s => SetCurrentBytes v idx (proj s)).
proof: Proof. eapply CorrectAlignedEncoderForProjection_Format with (format := format_word) (encoder := fun sz => @SetCurrentBytes sz n) (f := proj). eapply CorrectAlignedEncoderForFormatNChar; eauto. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Logic.Eqdep_dec Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Vectors.Vector Coq.ZArith.ZArith Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad