proposition: Lemma length_ByteString_Projection {S S'}: forall (format1 : FormatM S ByteString) (f : S' -> S) (b : ByteString) s (ctx ctx' : CacheFormat) (n : nat), (Projection_Format format1 f)%format s ctx ↝ (b, ctx') -> (forall (ctx0 : CacheFormat) (b0 : ByteString) (ctx'0 : CacheFormat), format1 (f s) ctx0 ↝ (b0, ctx'0) -> length_ByteString b0 = n) -> length_ByteString b = n.
proof: Proof. intros. eapply H0. eapply EquivFormat_Projection_Format; 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