proposition: Lemma refine_Pick_If_Then_Opt {A B} : forall (P : Ensemble B) (c e : Comp A) (t : B -> Comp A), (forall b, P b -> refine c (t b)) -> (refine c e) -> refine c (b <- {b | forall b', (b = Some b' -> P b')}; Ifopt b as b' Then t b' Else e).
proof: Proof. t_refine. destruct v0; t_refine. eapply H; eauto. 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