proposition: Lemma refine_format_enum : forall idx ce, refine (format_enum idx ce) (ret (encode_enum idx ce)).
proof: Proof. intros; reflexivity. Qed.
imports: Fiat.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Coq.Vectors.Vector Bedrock.Word