proposition: Lemma length_ByteString_composeIf {S} : forall format1 format2 b s (ctx ctx' : CacheFormat) n, computes_to (composeIf format1 format2 s ctx) (b, ctx') -> (forall (s : S) ctx b ctx', computes_to (format1 s ctx) (b, ctx') -> length_ByteString b = n) -> (forall (s : S) ctx b ctx', computes_to (format2 s ctx) (b, ctx') -> length_ByteString b = n) -> length_ByteString b = n.
proof: Proof. unfold composeIf, Union_Format, Bind2; intros; computes_to_inv; injections. rewrite unfold_computes in H; destruct_ex. revert H H0 H1; pattern x; apply IterateBoundedIndex.Iterate_Ensemble_BoundedIndex_equiv; simpl. repeat apply IterateBoundedIndex.Build_prim_and; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.Option Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.InternetChecksum Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats Bedrock.Word