proposition: Lemma CorrectAlignedEncoderProjection {S S' : Type} {cache : Cache} (format_S : FormatM S' ByteString) (f : S -> S') (encode : forall sz, AlignedEncodeM sz) : CorrectAlignedEncoder format_S encode -> CorrectAlignedEncoder (Projection_Format format_S f) (Projection_AlignedEncodeM encode f).
proof: Proof. intros H; destruct H as [? [? [? ?] ] ]. eexists (Basics.compose x f); intuition. - intros; intros ? ?. eapply H in H3. unfold Projection_Format, Compose_Format; apply unfold_computes; eexists; split; eauto. apply H2. - unfold Projection_Format, Compose_Format in H3. rewrite @unfold_computes in H3; destruct_ex; intuition. eapply H in H2; eauto. subst; eauto. - eapply H0. unfold Basics.compose in H2; eauto. - unfold EncodeMEquivAlignedEncodeM, Basics.compose; intuition. + eapply H1; eauto. + edestruct H1 as [? [? [? ?] ] ]. eapply H5; eassumption. + edestruct H1 as [? [? [? ?] ] ]. eapply H6; eassumption. + edestruct H1 as [? [? [? ?] ] ]. eapply H6; eassumption. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString