proposition: Lemma refine_bind_pick : forall (A B : Type) (P : Ensemble A), forall x y : A -> Comp B, (forall a, P a -> refine (x a) (y a)) -> refine (a <- {a | P a}; x a) (a <- {a | P a}; y a).
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