fact: Definition pull_match_sumbool {L R : Prop} {A B} (P : A -> B) (a : L -> A) (a' : R -> A) (b : sumbool L R) : P (match b with | left x => a x | right x => a' x end) = match b with | left x => P (a x) | right x => P (a' x) end := pull_match_sumbool_dep (fun _ => P) a a' b.
imports: Fiat.Common.Coq__8_4__8_5__Compat