fact: Definition pull_option_rect {T A B} (P : A -> B) (a : T -> A) (a' : A) (x : option T) : P (option_rect (fun _ => A) a a' x) = option_rect (fun _ => B) (fun x => P (a x)) (P a') x := pull_option_rect_dep (fun _ => P) a a' x.
imports: Fiat.Common.Coq__8_4__8_5__Compat