proposition: Lemma refine_pick_decides_branches {A} (P : Prop) (Q Q' : Ensemble A) (q q' : Comp A) : (P -> refine {a | Q a} q) -> (~ P -> refine {a | Q' a} q') -> refine {a | (P -> Q a) /\ (~ P -> Q' a)} (b <- {b | decides b P}; If b Then q Else q').
proof: Proof. intros; eapply refine_pick_decides. - unfold refine; intros; computes_to_inv; econstructor; intuition; eapply H4; eauto. - unfold refine; intros; computes_to_inv; econstructor; intuition; eapply H4; 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