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