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