proposition: Lemma CorrectAlignedEncoderForFormatChar : CorrectAlignedEncoder (format_word (monoidUnit := ByteString_QueueMonoidOpt)) (@SetCurrentByte _ _).
proof: Proof. replace (@SetCurrentByte _ _) with (fun (sz : nat) v idx s => SetCurrentByte (n := sz) v idx (id s)). eapply refine_CorrectAlignedEncoder. 2: eapply (CorrectAlignedEncoderForFormatChar_f id). split; intros. + unfold Projection_Format, Compose_Format. intros v Comp_v; rewrite unfold_computes in Comp_v; destruct_ex; intuition. subst; eauto. + intro; apply (H v). unfold Projection_Format, Compose_Format in *. rewrite unfold_computes; eexists. subst; eauto. + eapply functional_extensionality_dep; intros. repeat (eapply functional_extensionality; intros). reflexivity. 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