proposition: Lemma length_ByteString_compose: forall (format1 format2 : CacheFormat -> Comp (ByteString * CacheFormat)) (b : ByteString) (ctx ctx' : CacheFormat) (n n' : nat), (format1 ThenC format2) ctx ↝ (b, ctx') -> (forall (ctx0 : CacheFormat) (b0 : ByteString) (ctx'0 : CacheFormat), format1 ctx0 ↝ (b0, ctx'0) -> length_ByteString b0 = n) -> (forall (ctx0 : CacheFormat) (b0 : ByteString) (ctx'0 : CacheFormat), format2 ctx0 ↝ (b0, ctx'0) -> length_ByteString b0 = n') -> length_ByteString b = n + n'.
proof: Proof. intros. unfold compose, Bind2 in H; computes_to_inv. destruct v; destruct v0; simpl in *; injections. erewrite length_ByteString_enqueue_ByteString, H0, H1; eauto with arith. 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