proposition: Corollary refine_IfDec_true : forall (P : Prop) ResultT (t e : Comp ResultT), P -> refine (IfDec P Then t Else e) t.
proof: Proof. intros; rewrite refine_IfDec with (b := true); simpl; eauto. reflexivity. Qed.
imports: Fiat.Common Fiat.Computation.Decidable Fiat.Computation.Core Fiat.Computation.Refinements.General Fiat.Computation.Monad Fiat.Computation.Refinements.General