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