proposition: Lemma refine_iff_P A : forall (Pc : Prop) (Pt Pa : Ensemble A), refine { a | (Pc -> Pt a) /\ Pa a} (b <- {b | decides b Pc}; If b Then { a | Pt a /\ Pa a} Else { a | Pa a}).
proof: Proof. intros * v Comp_v; computes_to_inv. computes_to_econstructor; intuition; subst; try destruct v0; simpl in *; eauto; computes_to_inv; intuition. 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