proposition: Lemma refine_bind_bind_dep' X Y Z (f : X -> Comp Y) (g : Y -> X -> Comp Z) x : refine (Bind x (fun x0 => Bind (f x0) (fun u => g u x0))) (Bind (Bind x (fun x0 => Bind (f x0) (fun u => ret (u, x0)))) (fun x0u => g (fst x0u) (snd x0u))).
proof: Proof. red; intros. computes_to_inv; subst. eauto using @BindComputes. Qed.
imports: Fiat.QueryStructure.Automation.MasterPlan Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Fiat.Narcissus.Formats.ByteBuffer Bedrock.Word Fiat.Narcissus.BinLib.Core