proposition: Lemma refine_format_unused_word {S} : forall sz (s : S) ce, refine (format_unused_word sz s ce) (format_word (wzero sz) ce).
proof: Proof. intros; unfold format_unused_word, Compose_Format; intros ? ?. apply unfold_computes; eexists; split; eauto. 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