proposition: Lemma refine_decide_negation : forall {A} (P: A -> Prop), refine (Pick (fun (b : bool) => decides b (forall (x: A), ~ P x))) (Bind (Pick (fun b => decides b (exists (x: A), P x))) (fun b => ret (negb b))).
proof: Proof. intros; rewrite refine_decide_not, refine_decide_negb; reflexivity. 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