proposition: Lemma refine_IfDec_decides : forall `{Decidable P} ResultT (t e : Comp ResultT), refineEquiv (IfDec P Then t Else e) (If Decidable_witness Then t Else e).
proof: Proof. split; intros. - apply refine_IfDec; eauto. case_eq (@Decidable_witness _ H); simpl. + intros; eapply Decidable_spec; eauto. + intros; eapply Decidable_complete_alt; eauto. - unfold IfDec_Then_Else, If_Then_Else, refine; intros; computes_to_inv. destruct v0. + simpl in H0; apply Decidable_spec in H0; rewrite H0; eauto. + simpl in H0; eapply Decidable_sound_alt in H0; rewrite H0; eauto. Qed.
imports: Fiat.Common Fiat.Computation.Decidable Fiat.Computation.Core Fiat.Computation.Refinements.General Fiat.Computation.Monad Fiat.Computation.Refinements.General