proposition: Lemma CorrectAlignedEncoderForProjection_Format {S S'} (f : S -> S') (format : FormatM S' ByteString) (encoder : forall n, AlignedEncodeM n) : CorrectAlignedEncoder format encoder -> CorrectAlignedEncoder (Projection_Format format f) (fun sz v idx (s : S) => encoder sz v idx (f s)).
proof: Proof. intros; eapply refine_CorrectAlignedEncoder. split; intros. - rewrite refine_Projection_Format at 1. higher_order_reflexivity. - intro. eapply H. apply refine_Projection_Format in H0. eauto. - destruct X; intuition. eexists (fun s env => x (f s) env); intuition eauto. eapply H; eauto. eapply H; eauto. unfold EncodeMEquivAlignedEncodeM in *; intros. specialize (H2 env (f s) idx); intuition 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