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