proposition: Lemma CorrectAlignedEncoderForDoneC : CorrectAlignedEncoder (fun s e => Return (ByteString_id, e)) AlignedEncode_Nil.
proof: Proof. unfold CorrectAlignedEncoder; intros. eexists (fun _ env => Some (ByteString_id, env)); split; [ | split]; intros. - split; intros. + congruence. + congruence. - injections; reflexivity. - eapply Return_EncodeMEquivAlignedEncodeM. 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