proposition: Lemma refine_IfDec : forall (P : Prop) b ResultT (t e : Comp ResultT), decides b P -> refine (IfDec P Then t Else e) (If b Then t Else e).
proof: Proof. intros. unfold IfDec_Then_Else. refine pick val b; eauto. rewrite refineEquiv_bind_unit; reflexivity. Qed.
imports: Fiat.Common Fiat.Computation.Decidable Fiat.Computation.Core Fiat.Computation.Refinements.General Fiat.Computation.Monad Fiat.Computation.Refinements.General