proposition: Lemma refine_pick_decides {A} : forall (P : Prop) (c e : Comp A) (t : Comp A), (P -> refine c t) -> (~ P -> refine c e) -> refine c (b <- {b | decides b P}; If b Then t Else e).
proof: Proof. unfold refine; intros; computes_to_inv; destruct_ex; split_and; computes_to_inv. destruct v0; simpl in *; eauto. 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