proposition: Lemma EncodeMEquivAlignedEncodeM_word_const {S} {n} : forall (w : word (n*8)), EncodeMEquivAlignedEncodeM (fun (_ : S) env => Some (encode_word' _ w mempty, addE env (n*8))) (encode_word_const w).
proof: Proof. intros. destruct CorrectAlignedEncoderForFormatNChar with (sz:=n); eauto. destruct_conjs. eapply EncodeMEquivAlignedEncodeM_const in H1. match goal with | H : EncodeMEquivAlignedEncodeM ?a _ |- EncodeMEquivAlignedEncodeM ?b _ => replace b with a end. eauto. extensionality s. extensionality ce. eauto using format_word_is_encode_word. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Stores.EmptyStore Bedrock.Word