proposition: Lemma refine_under_bind_helper_1 X Y (f : X -> Comp Y) x x' y : (forall y, refine x y -> refine x' 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