fact: Definition pull_option_rect_dep {T A B} (P : forall x : option T, A x -> B x) (a : forall x, A (Some x)) (a' : A None) (x : option T) : P x (option_rect A a a' x) = option_rect B (fun x => P _ (a x)) (P _ a') x := match x with Some _ => eq_refl | None => eq_refl end.
imports: Fiat.Common.Coq__8_4__8_5__Compat