fact: Definition option_rect_const {A B} (a a' : B) (x : option A) : option_rect (fun _ => B) (fun _ => a) a' x = bool_rect (fun _ => B) a a' (option_rect _ (fun _ => true) false x) := match x with Some _ => eq_refl | None => eq_refl end.
imports: Fiat.Common.Coq__8_4__8_5__Compat