proposition: Lemma refineEquiv_ThenC {A B Env} {monoid : Monoid B} : forall (format1 : A -> Env -> Comp (B * Env)) (format2 : A -> Env -> Comp (B * Env)) {A' A''} (f : A -> A') (f' : A -> A'') (format1' : A' -> Env -> Comp (B * Env)) (format2' : A'' -> Env -> Comp (B * Env)) (format' : (A' * A'') -> Env -> Comp (B * Env)) (H1 : forall a env, refineEquiv (format1 a env) (format1' (f a) env)) (H2 : forall a env, refineEquiv (format2 a env) (format2' (f' a) env)) (H' : forall aa' env, format' aa' env = (format1' (fst aa') ThenC (format2' (snd aa'))) env) (a : A) (env : Env), refineEquiv ((format1 a ThenC format2 a) env) (format' ((fun a => (f a, f' a)) a) env).
proof: Proof. intros; unfold compose, Bind2; intros; setoid_rewrite H'; setoid_rewrite H1; setoid_rewrite H2; reflexivity. 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