proposition: Lemma refine_decide_not : forall {A} (P: A -> Prop), refine (Pick (fun (b : bool) => decides b (forall (x: A), ~ P x))) (Pick (fun (b : bool) => decides (negb b) (exists (x: A), P x))).
proof: Proof. unfold refine; intros; computes_to_inv. computes_to_constructor. rewrite <- not_exists_forall; apply decides_negb; assumption. 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