proposition: Lemma refine_format_compose_map sz {S S' S''} (format_S'' : FormatM S'' _) (f : S -> S') (g : S' -> S'') (f' : S -> word sz) (refine_proj : forall (s : S) (env : CacheFormat), refine (FMapFormat.Projection_Format format_S'' (Basics.compose g f) s env) ((format_word ◦ f') s env)) : forall s ce, refine (FMapFormat.Projection_Format (FMapFormat.Projection_Format format_S'' g) f s ce) (FMapFormat.Projection_Format format_word f' s ce).
proof: Proof. intros; rewrite <- refine_proj. intros; unfold FMapFormat.Projection_Format, FMapFormat.Compose_Format; intros ? ?. rewrite unfold_computes in H; destruct_ex; intuition. apply unfold_computes; eexists; split; eauto; subst. apply unfold_computes. eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Narcissus.BinLib Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Automation.NormalizeFormats Bedrock.Word