proposition: Lemma refine_format_word_map {S} {sz} (f : S -> word sz) : forall s ce, refine (FMapFormat.Projection_Format format_word f s ce) (format_word (f s) ce).
proof: Proof. intros; unfold FMapFormat.Projection_Format, FMapFormat.Compose_Format; intros ? ?. apply unfold_computes; eexists; split; 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