proposition: Lemma decides_negb : forall b P, decides (negb b) P -> decides b (~ P).
proof: Proof. unfold decides; setoid_rewrite if_negb; simpl; intros. destruct b; simpl in *; 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