proposition: Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v, option_rect (fun _ => C) (fun x => some (f x)) none v = option_rect (fun _ => C) some none (option_map f v).
proof: Proof. destruct v; reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Relations.Relation_Definitions Fiat.Common.Coq__8_4__8_5__Compat