proposition: Lemma EquivFormat_compose_map {S S' S'' T} (format_S'' : FormatM S'' T) (f : S -> S') (g : S' -> S'') : EquivFormat (Projection_Format (Projection_Format format_S'' g) f) (Projection_Format format_S'' (Basics.compose g f)).
proof: Proof. unfold EquivFormat, refineEquiv, Projection_Format, Compose_Format, compose, Bind2; split; intros ? ?. - rewrite unfold_computes in *. destruct_ex; split_and; eexists. rewrite unfold_computes; eauto. - rewrite unfold_computes in *. destruct_ex; split_and; eexists; intuition eauto. rewrite unfold_computes in H0. destruct_ex. intuition eauto. subst. apply H0. 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