fact: Definition pull_bool_rect_dep {A B} (P : forall b : bool, A b -> B b) (a : A true) (a' : A false) (b : bool) : P b (bool_rect A a a' b) = bool_rect B (P _ a) (P _ a') b := match b with true => eq_refl | false => eq_refl end.
imports: Fiat.Common.Coq__8_4__8_5__Compat