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