proposition: Lemma length_ByteString_map_option {S S'} : forall (sz : nat) (f : S -> option S') (format_Some : FormatM S' _) (format_None : FormatM () _) (s : S) (b : ByteString) (ctx ctx' : CacheFormat), (forall s', format_Some s' ctx ∋ (b, ctx') -> length_ByteString b = sz) -> (format_None () ctx ∋ (b, ctx') -> length_ByteString b = sz) -> Projection_Format (Option.format_option format_Some format_None) f s ctx ∋ (b, ctx') -> length_ByteString b = sz.
proof: Proof. unfold Projection_Format, Compose_Format; intros. rewrite unfold_computes in H1; destruct_ex; intuition; subst. destruct (f s); simpl in *; 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