proposition: Lemma refineEquiv_bind_unit X Y (f : X -> Comp Y) x : refineEquiv (Bind (Return x) f) (f x).
proof: Proof. split; intro; simpl; apply bind_unit. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Fiat.Common Fiat.Computation.Core