proposition: Lemma refineEquiv_bind2_unit A B C (f : A -> B -> Comp C) x : refineEquiv (Bind2 (Return x) f) (f (fst x) (snd x)).
proof: Proof. unfold Bind2; split; intros; destruct x; simpl. rewrite refine_bind_unit; reflexivity. rewrite <- refine_bind_unit'; reflexivity. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Fiat.Common Fiat.Computation.Core