proposition: Lemma refineEquiv_bind_bind X Y Z (f : X -> Comp Y) (g : Y -> Comp Z) x : refineEquiv (Bind (Bind x f) g) (Bind x (fun u => Bind (f u) g)).
proof: Proof. split; intro; apply bind_bind. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Fiat.Common Fiat.Computation.Core