proposition: Lemma refine_pick_eq_ex_bind {A B : Type} (P : A -> B -> Prop) (a : A) : refine (a' <- {a' | a' = a /\ exists b, P a' b}; {b | P a' b}) {b | P a b}.
proof: Proof. t_refine. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Bool.Bool Fiat.Common Fiat.Common.BoolFacts Fiat.Common.LogicFacts Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.SetoidMorphisms Fiat.Computation.Refinements.Tactics