proposition: Lemma CorrectAlignedEncoder2CorrectEncoder {A} {cache : Cache.Cache} (FormatSpec : Specs.FormatM A _) (encoder : CorrectAlignedEncoderFor FormatSpec) : Specs.CorrectEncoderFor FormatSpec.
proof: Proof. eexists (projT1 (projT2 encoder)); split; intros; destruct encoder as [aligned_encoder [encoder [encoder_OK [padding_OK encoder_equiv] ] ] ]. - destruct benv'. eapply encoder_OK; eauto. - simpl in *. eapply encoder_OK; eauto. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Monoid Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedByteBuffer Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedIPChecksum