proposition: Lemma refineEquiv_bind2_bind A B C D Z (f : A -> B -> Comp (C * D)) (g : C ->D -> Comp Z) x : refineEquiv (Bind2 (Bind2 x f) g) (Bind2 x (fun a b => Bind2 (f a b) g)).
proof: Proof. split; intro; apply bind_bind. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Fiat.Common Fiat.Computation.Core