proposition: Lemma refine_decide_negb : forall P, refineEquiv (Pick (fun b => decides (negb b) P)) (Bind (Pick (fun b => decides b P)) (fun b => ret (negb b))).
proof: Proof. unfold refineEquiv, refine; simpl; split; intros; computes_to_inv; subst; repeat computes_to_econstructor; eauto; rewrite Bool.negb_involutive; [ assumption | constructor ]. 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