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