proposition: Lemma CorrectAlignedEncoderForFormatUnusedWord {S} : CorrectAlignedEncoder (format_unused_word 8 (monoidUnit := ByteString_QueueMonoidOpt)) (fun sz v idx (s : S) => SetCurrentByte v idx (wzero 8)).
proof: Proof. intros; eapply refine_CorrectAlignedEncoder; eauto using (CorrectAlignedEncoderForFormatChar_f (fun _ => wzero 8)). simpl; split; intros. + unfold format_unused_word, Projection_Format, Compose_Format; simpl. intros ? ?. rewrite unfold_computes in *. destruct_ex; split_and; subst. eexists; split; eauto. rewrite unfold_computes; eauto. + unfold format_unused_word, Projection_Format, Compose_Format; simpl. intros ?. eapply (H _). unfold format_unused_word, Projection_Format, Compose_Format; simpl. destruct_ex; split_and; subst. rewrite unfold_computes; eauto. eexists _; split; eauto. unfold format_word; 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