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