proposition: Lemma refine_bind_pick {A B} : forall (P : A -> Prop) (c : Comp B) (c' : A -> Comp B), (forall a', P a' -> refine c (c' a')) -> refine c (a <- {a | P a}; c' a).
proof: Proof. unfold refine; intros. computes_to_inv; eauto. Qed.
imports: Fiat.Common Fiat.Computation.Core Fiat.Computation.SetoidMorphisms Fiat.ADT Coq.Lists.List