proposition: Lemma refine_bind_bind_helper X Y Z (f : X -> Comp Y) (g : Y -> Comp Z) x y : refine (Bind x (fun u => Bind (f u) g)) y -> refine (Bind (Bind x f) g) y.
proof: Proof. t. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Fiat.Common Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.SetoidMorphisms