proposition: Lemma refine_under_bind_helper_2 X Y (f f' : X -> Comp Y) x y : (forall x0 y, refine (f x0) y -> refine (f' x0) y) -> refine (Bind x f) y -> refine (Bind x f') y.
proof: Proof. t2. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Fiat.Common Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.SetoidMorphisms