proposition: Lemma sequence_mempty' {S T : Type} {store : Cache} {m : Monoid T} : forall (format : FormatM S T), EquivFormat (format ++ empty_Format) format.
proof: Proof. unfold sequence_Format, EquivFormat, empty_Format; intros. split; unfold compose, Bind2; intros v Comp_v. - computes_to_econstructor; eauto. destruct_conjs; simpl. computes_to_econstructor; eauto. simpl. rewrite mempty_right; eauto. - computes_to_inv; subst; destruct_conjs. simpl. rewrite mempty_right; eauto. Qed.
imports: Coq.Bool.Bool Coq.ZArith.ZArith Fiat.Common.DecideableEnsembles Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.Tactics.CacheStringConstant Fiat.Common.IterateBoundedIndex Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.Option Fiat.Narcissus.Formats.Empty Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Common.Sig