fact: Definition pull_bool_rect {A B} (P : A -> B) (a a' : A) (b : bool) : P (bool_rect (fun _ => A) a a' b) = bool_rect (fun _ => B) (P a) (P a') b := pull_bool_rect_dep (fun _ => P) a a' b.
imports: Fiat.Common.Coq__8_4__8_5__Compat