proposition: Lemma refine_sumbool_bind : forall `(P : {A} + {~A}) `(f : A -> Comp B) (g : ~A -> Comp B) `(h : B -> Comp C), refine (x <- match P with | left H => f H | right H => g H end; h x) (match P with | left H => x <- f H; h x | right H => x <- g H; h x end).
proof: Proof. t2 P. 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