proposition: Lemma refineEquiv_unit_bind2 A B (x : Comp (A * B)) : refineEquiv (Bind2 x (fun x y => Return (x, y))) x.
proof: Proof. unfold Bind2; split; intros; simpl. intros v Comp_v; computes_to_econstructor; eauto; destruct v; eauto. intros v Comp_v; computes_to_inv; subst; destruct v0; eauto. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Fiat.Common Fiat.Computation.Core