proposition: Lemma refine_pick_val' : forall {A : Type} (a : A) (P : A -> Prop), P a -> refine (Pick P) (ret a).
proof: Proof. intros; apply refine_pick_val; assumption. 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