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