proposition: Lemma length_ByteString_bool : forall (b : bool) (bs : ByteString) (ctx ctx' : CacheFormat), format_bool b ctx ↝ (bs, ctx') -> length_ByteString bs = 1.
proof: Proof. unfold format_bool; intros; computes_to_inv; injections. reflexivity. 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